Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
51 check-ins using file bs/builtins/statements/if.cpp version ee82b1943e
|
2019-11-18
| ||
| 01:40 | Verifier: first seemingly working version of the k-induction loop checker. check-in: 477ef5b3d4 user: achavasse tags: trunk | |
|
2019-11-17
| ||
| 18:20 |
| |
|
2019-11-16
| ||
| 16:27 |
| |
|
2019-11-08
| ||
| 11:48 | Verifier: check assertions with z3 immediately instead of postponing it until we have built the entire formula for the function. check-in: e33c4ea6c1 user: achavasse tags: trunk | |
|
2019-11-04
| ||
| 19:53 | Verifier: more work on loop verification. check-in: b4385d9930 user: achavasse tags: trunk | |
|
2019-10-30
| ||
| 22:09 | Removed an obsolete comment. check-in: 626057ff22 user: achavasse tags: trunk | |
| 22:08 | Verifier: more work on loop verification. check-in: c91249ffc7 user: achavasse tags: trunk | |
|
2019-10-27
| ||
| 21:31 | Verifier: split func.cpp into multiple files to make navigation easier. check-in: f606dd6e5d user: achavasse tags: trunk | |
|
2019-10-22
| ||
| 22:11 | Verifier: traverse basic blocks in breadth first order and make sure that the current block's predecessors are processed first, so that we don't rely anymore on the order in which they are created by the statements. check-in: d7e2fcc24f user: achavasse tags: trunk | |
|
2019-10-20
| ||
| 14:13 | Verifier: more work on loop unrolling. check-in: 8082ea7f42 user: achavasse tags: trunk | |
|
2019-10-18
| ||
| 11:33 |
Verifier:
| |
|
2019-10-16
| ||
| 23:08 | llr: detect and store relevant informations about loops in the CFG to be able to unroll them in the verifier. check-in: b1f107d1e7 user: achavasse tags: trunk | |
|
2019-10-15
| ||
| 00:04 | llr: implemented a helper function to compute dominators. check-in: cfc94e192c user: achavasse tags: trunk | |
|
2019-10-12
| ||
| 17:25 | Verifier: use z3 push/pop to check assertions one at a time, so that we can find and report multiple errors in the same function. check-in: b414bc18df user: achavasse tags: trunk | |
|
2019-10-11
| ||
| 22:24 | Docs: add anchors on sub section titles. check-in: 4f4a1dc4aa user: achavasse tags: trunk | |
|
2019-10-10
| ||
| 01:00 | Docs: typo fix. check-in: d167a0b946 user: achavasse tags: trunk | |
| 00:38 | Some docs fixes. check-in: e36fbebe18 user: achavasse tags: trunk | |
| 00:26 | Wrote some docs. check-in: 8f046020b6 user: achavasse tags: trunk | |
|
2019-10-09
| ||
| 19:42 | Added .editorconfig file. check-in: ed08ba02f2 user: achavasse tags: trunk | |
| 19:34 | Some more renaming. check-in: f65c08a1c5 user: achavasse tags: trunk | |
| 19:21 | Some renaming for consistency and to match commonly used names for those things. check-in: 5e72e8e08c user: achavasse tags: trunk | |
|
2019-10-08
| ||
| 21:55 |
| |
| 18:17 | Expose "@" as a placeholder for the function's return value inside of ensures statements. check-in: 8541259c1c user: achavasse tags: trunk | |
| 18:02 | Added the "placeholder" llr pseudo instruction. check-in: cc9ce06e64 user: achavasse tags: trunk | |
|
2019-10-07
| ||
| 22:04 | Made the "assertion failure" error message lowercase to be consistent with other error messages. check-in: acbb4b30b8 user: achavasse tags: trunk | |
| 21:58 |
| |
|
2019-10-05
| ||
| 16:37 |
| |
| 14:50 | verification: implemented a trace mode that only dumps the z3 expressions. check-in: 0b95fe304a user: achavasse tags: trunk | |
| 13:58 | Implemented the conversion of GetVar/SetVar/GetTemporary/SetTemporary to z3 expressions. check-in: 3ae3c0b3ad user: achavasse tags: trunk | |
| 11:55 | z3 builder: handle variables. check-in: 83476a562e user: achavasse tags: trunk | |
|
2019-10-03
| ||
| 20:01 | Removed an obsolete TODO. check-in: 251bfddf8b user: achavasse tags: trunk | |
| 19:58 | FuncValidator: model the execution flow in z3 by generating boolean expressions describing when each basic block is executed. check-in: 6c8e8075ff user: achavasse tags: trunk | |
|
2019-10-02
| ||
| 22:15 | Typo fix. check-in: 57129c3f9a user: achavasse tags: trunk | |
| 22:11 | z3 builder: instead of directly adding negated assertions to the solver, gather them into a conjunction and add that. check-in: 2734029a31 user: achavasse tags: trunk | |
| 20:09 | FuncValidator: more work on the implementation. check-in: 98a85945f6 user: achavasse tags: trunk | |
| 19:30 | Implemented a helper class allowing to wrap each z3 expression with a predicate indicating that the execution flow went through a certain basic block. check-in: 1d340c945f user: achavasse tags: trunk | |
|
2019-09-30
| ||
| 21:50 | Began the implementation of the function verifier. check-in: a0c53b4adb user: achavasse tags: trunk | |
|
2019-09-29
| ||
| 23:11 | repo: don't attempt to perform syntax highlighting on text files. check-in: be610f458b user: achavasse tags: trunk | |
| 22:30 |
| |
| 20:30 | Added a specific llr instruction for 'not' for the sake of constructing z3 expressions. check-in: 2628782ef2 user: achavasse tags: trunk | |
|
2019-09-26
| ||
| 23:37 | Refactored the parsing of verification statements so that it works properly in all cases (regular functions, template functions, function type expressions, lambdas). check-in: 4fe418f4d0 user: achavasse tags: trunk | |
| 00:27 | Static analysis: check that function verification statements are satisfiable and emit relevant error messages if they aren't. check-in: 7f14d60722 user: achavasse tags: trunk | |
|
2019-09-25
| ||
| 19:16 | Implemented a first batch of llr instruction to z3 expression conversions. check-in: b6b76a4e03 user: achavasse tags: trunk | |
|
2019-09-24
| ||
| 22:06 | Began writing the static analyzer. check-in: d960d10be9 user: achavasse tags: trunk | |
| 19:52 | Fix wrong file deletion. check-in: 103523bfe9 user: achavasse tags: trunk | |
| 19:50 | Updated repo's syntax highlighting theme. check-in: 2aafe4e645 user: achavasse tags: trunk | |
| 19:13 | Updated repo's syntax highlighting. check-in: af5df97f63 user: achavasse tags: trunk | |
|
2019-09-23
| ||
| 21:35 | build: find the z3 library. check-in: b3c85287b1 user: achavasse tags: trunk | |
| 21:00 | verification stmts: append to the assertion lists, instead of overwriting them. check-in: db3875c530 user: achavasse tags: trunk | |
|
2019-09-22
| ||
| 22:42 | Implemented overloads of boolean or/and operators for verification expressions that don't do shortcut evaluation but simply emit the corresponding llr instruction. check-in: 7dcd0447a3 user: achavasse tags: trunk | |
| 14:37 | Project renaming. check-in: af650a9e95 user: achavasse tags: trunk | |