Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
17 check-ins using file bs/verify/verify.h version 72fc02c0e2
|
2020-01-27
| ||
| 00:24 | Refinement types: parse predicates lazily to play well with templates. check-in: e57c63fea5 user: achavasse tags: trunk | |
|
2020-01-23
| ||
| 22:24 | Refinement types: implemented the where operator to add predicates to a type. check-in: 9586391cdb user: achavasse tags: trunk | |
|
2020-01-22
| ||
| 22:14 | Standardized the way type values are encoded to make room for an optional pointer to a list of predicates for refinement types. check-in: cc380f4f8f user: achavasse tags: trunk | |
|
2020-01-16
| ||
| 21:41 | ir: also make void* always compare to true to make it easier to work with llvm type pointers embedded inside type IR expressions. check-in: 6680e30102 user: achavasse tags: trunk | |
| 20:46 | ir: comparing ptr< void > is considered always true, to allow to more easily attach opaque data onto ir expressions without changing their semantics. check-in: 1a704c5a51 user: achavasse tags: trunk | |
|
2020-01-13
| ||
| 23:13 | Renamed the runtime struct type to "record" to avoid future confusion since it's a much lower level type (essentially just a tuple restricted to runtime types) than the future "struct" type. check-in: b573d100cf user: achavasse tags: trunk | |
|
2020-01-12
| ||
| 21:10 | builtins: added wrapper types to allow terms and values to be manipulated at low level within the language itself. check-in: ceb0b190d6 user: achavasse tags: trunk | |
| 20:03 | builtins: added a wrapper for a CodeBuilder pointer. check-in: d4e5c46e57 user: achavasse tags: trunk | |
|
2020-01-11
| ||
| 18:28 |
| |
|
2020-01-05
| ||
| 21:46 | Fix (inconsequential) missing else. check-in: 9ad87f2dcf user: achavasse tags: trunk | |
| 20:22 |
| |
| 17:41 | Simplified the implementation of the comma operator. check-in: a25bb3bc5f user: achavasse tags: trunk | |
|
2020-01-04
| ||
| 23:44 |
| |
| 18:27 | Verification: changed the syntax for the current function's return value to the more explicit "@result". check-in: cbbd282cfa user: achavasse tags: trunk | |
| 17:28 | Loop verifier: when still finding counter-examples at max K unrolls, emit error messages for the failed conditions instead of a generic "couldn't verify loop" message. check-in: 23d2aa4c8a user: achavasse tags: trunk | |
| 15:48 | Verifier: tweak the wording of the unsatisfiability error for consistency, also sort those by location ids to have a deterministic output. check-in: 264e55dac8 user: achavasse tags: trunk | |
| 15:17 |
| |