test-branch : lp:cbmc : Git : Code : CBMC

Branch information

3289add... by TGWDB <email address hidden> on 2023-04-03

Merge pull request #7645 from NlightNFotis/rust_verification_result

Translate verification results from C++ to Rust

193b2fd... by =?utf-8?q?R=C3=A9mi_Delmas?= <email address hidden> on 2023-04-03

Merge pull request #7628 from remi-delmas-3000/contracts-contract-mode

CONTRACTS: add loop contract mode enum and string conversion functions

a1eb073... by Fotis Koutoulakis <email address hidden> on 2023-04-03

Add documentation and extra tests for querying for non-existent properties

d8a78cc... by Remi Delmas <email address hidden> on 2023-03-23

CONTRACTS: add loop contract mode enum and string conversion functions

Used by loop contracts and error messages.

e3a7dcf... by Fotis Koutoulakis <email address hidden> on 2023-04-03

Translate verification results from C++ to Rust,

and add a test for covering that.

4413298... by Michael Tautschnig <email address hidden> on 2023-04-03

Merge pull request #7642 from tautschnig/cleanup/read_bin_goto_object

Cleanup read_bin_goto_object

6933f01... by Michael Tautschnig <email address hidden> on 2023-04-03

Cleanup read_bin_goto_object

Remove unnecessary braces that obscure control flow, and remove
commented-out code that has no use.

f8380e5... by =?utf-8?q?R=C3=A9mi_Delmas?= <email address hidden> on 2023-04-01

Merge pull request #7631 from remi-delmas-3000/contracts-loop-nesting-graph

CONTRACTS: represent loop nesting structure as a graph

b4b59d9... by Remi Delmas <email address hidden> on 2023-03-23

CONTRACTS: represent loop nesting structure as a graph

Utility class for loop contracts instrumentation.

9161eae... by =?utf-8?q?R=C3=A9mi_Delmas?= <email address hidden> on 2023-04-01

Merge pull request #7630 from remi-delmas-3000/contracts-is-cprover-symbol

CONTRACTS: is_cprover_symbol utility function

»