File tree Expand file tree Collapse file tree
liquidjava-example/src/main/java/testSuite/classes
resultset_forward_correct
liquidjava-verifier/src/main/java/liquidjava
processor/refinement_checker Expand file tree Collapse file tree Original file line number Diff line number Diff line change 33import liquidjava .specification .ExternalRefinementsFor ;
44import liquidjava .specification .Ghost ;
55import liquidjava .specification .Refinement ;
6- import liquidjava .specification .RefinementAlias ;
76import liquidjava .specification .StateRefinement ;
8- import liquidjava .specification .StateSet ;
97
108import java .nio .ByteBuffer ;
11- import java .nio .ByteOrder ;
12- import java .nio .CharBuffer ;
13- import java .nio .ShortBuffer ;
14- import java .nio .IntBuffer ;
15- import java .nio .LongBuffer ;
16- import java .nio .FloatBuffer ;
17- import java .nio .DoubleBuffer ;
189
1910
2011@ Ghost ("boolean arrayBacked" )
Original file line number Diff line number Diff line change 33import liquidjava .specification .ExternalRefinementsFor ;
44import liquidjava .specification .Ghost ;
55import liquidjava .specification .Refinement ;
6- import liquidjava .specification .RefinementAlias ;
76import liquidjava .specification .StateRefinement ;
8- import liquidjava .specification .StateSet ;
97
108import java .nio .ByteBuffer ;
11- import java .nio .ByteOrder ;
12- import java .nio .CharBuffer ;
13- import java .nio .ShortBuffer ;
14- import java .nio .IntBuffer ;
15- import java .nio .LongBuffer ;
16- import java .nio .FloatBuffer ;
17- import java .nio .DoubleBuffer ;
189
1910
2011@ Ghost ("boolean arrayBacked" )
Original file line number Diff line number Diff line change 11package testSuite .classes .iterator_queue_error ;
22
33import liquidjava .specification .ExternalRefinementsFor ;
4- import liquidjava .specification .Refinement ;
54import liquidjava .specification .StateRefinement ;
65import liquidjava .specification .StateSet ;
76
Original file line number Diff line number Diff line change 11package testSuite .classes .resultset_forward_correct ;
22
33import java .sql .ResultSet ;
4- import java .sql .SQLException ;
54
65import liquidjava .specification .ExternalRefinementsFor ;
76import liquidjava .specification .Ghost ;
87import liquidjava .specification .Refinement ;
9- import liquidjava .specification .StateRefinement ;
10- import liquidjava .specification .StateSet ;
118
129
1310@ Ghost ("boolean setBackwards" )
Original file line number Diff line number Diff line change 11package testSuite .classes .resultset_forward_error ;
22
33import java .sql .ResultSet ;
4- import java .sql .SQLException ;
54
65import liquidjava .specification .ExternalRefinementsFor ;
76import liquidjava .specification .Ghost ;
87import liquidjava .specification .Refinement ;
9- import liquidjava .specification .StateRefinement ;
10- import liquidjava .specification .StateSet ;
118
129
1310@ Ghost ("boolean setBackwards" )
Original file line number Diff line number Diff line change 55import java .util .stream .Collectors ;
66
77import liquidjava .diagnostics .TranslationTable ;
8- import liquidjava .processor .VCImplication ;
98import liquidjava .rj_language .Predicate ;
109import liquidjava .rj_language .ast .Expression ;
1110import liquidjava .rj_language .ast .formatter .VariableFormatter ;
Original file line number Diff line number Diff line change 77import liquidjava .diagnostics .errors .LJError ;
88import liquidjava .processor .context .Context ;
99import liquidjava .processor .refinement_checker .general_checkers .MethodsFunctionsChecker ;
10- import liquidjava .rj_language .Predicate ;
1110import liquidjava .utils .constants .Formats ;
12- import liquidjava .utils .constants .Types ;
1311import spoon .reflect .declaration .CtClass ;
1412import spoon .reflect .declaration .CtConstructor ;
1513import spoon .reflect .declaration .CtEnum ;
Original file line number Diff line number Diff line change 66import java .util .Map ;
77import java .util .stream .Collectors ;
88
9- import liquidjava .diagnostics .DebugLog ;
109import liquidjava .diagnostics .errors .LJError ;
1110import liquidjava .diagnostics .errors .NotFoundError ;
12- import liquidjava .processor .VCImplication ;
13- import liquidjava .rj_language .opt .VCSimplificationResult ;
1411import liquidjava .processor .context .AliasWrapper ;
1512import liquidjava .processor .context .Context ;
1613import liquidjava .processor .context .GhostFunction ;
Original file line number Diff line number Diff line change 11package liquidjava .rj_language .opt ;
22
3- import java .util .Objects ;
4-
53import liquidjava .processor .VCImplication ;
64
75/**
Original file line number Diff line number Diff line change 33import com .microsoft .z3 .ArithExpr ;
44import com .microsoft .z3 .ArrayExpr ;
55import com .microsoft .z3 .BoolExpr ;
6- import com .microsoft .z3 .EnumSort ;
76import com .microsoft .z3 .Expr ;
87import com .microsoft .z3 .FPExpr ;
98import com .microsoft .z3 .FuncDecl ;
You can’t perform that action at this time.
0 commit comments