Goose  Timeline

Advanced

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

26 check-ins using file bs/llr/branch.h version 5aa4d4e80d

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
  • Verifier: handle calls (assert the callee's preconditions and assume its postconditions)
  • Verifier: handle return value placeholder in the post conditions.
  • Verifier: fixes.
  • Verifier: context descriptions and locations can be attached to assertions.
  • Lexer: fix incorrect location length on integer literals.
  • Added some tests for successful and failed verification of functions pre-conditions and post-conditions.
 check-in: 09e8221436 user: achavasse tags: trunk
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
  • Fixed incorrect logic when generating z3 expressions to track the value of variables accross basic blocks.
  • Implemented basic error reporting for verification failure that highlights all the failed assertions.
  • Added a test program that demonstrates a simple case of failed static verification.
 check-in: 717a1ea6d4 user: achavasse tags: trunk
2019-10-05
16:37
  • Renamed the "assert" test helper function to "check".
  • Implemented a builtin "assert" intrinsic that emits an Assert instruction for the verifier.
  • Implemented a couple of tests to verify the generated z3 expressions for a couple of simple functions.
  • Fixed a few issues when building the z3 expressions.
 check-in: 3740e7a491 user: achavasse tags: trunk
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
  • Fixed some issues with implicit termination of void functions.
  • llr: give an index to each basic block, and keep track of back links towards previous blocks.
 check-in: 4ae6912760 user: achavasse tags: trunk
Fossil 2.26 [1205ec86cb] 2025-04-30 16:57:32
This page was generated in about 0.016s