CBMC

cbmc:map_type

  1. Git
  2. lp:cbmc
  3. map_type
Last commit made on 2022-09-02
Get this branch:
git clone -b map_type https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
map_type
Repository:
lp:cbmc

Recent commits

14cf4a9... by Daniel Kroening <email address hidden>

introduce __CPROVER_map type

This introduces C syntax for a type

  __CPROVER_map domain -> codomain

where domain is a list of types and codomain is a type. The type is
internal, for modeling purposes. It replaces arrays with size
__CPROVER_infinity, which are now deprecated.

ed19cf1... by Michael Tautschnig <email address hidden>

Merge pull request #7047 from diffblue/shortcircuit

goto-convert: introduce assignment_lhs_needs_temporary

117fd9f... by Thomas Spriggs <email address hidden>

Merge pull request #7078 from thomasspriggs/tas/smt_array_trace_printing_extended

Add array trace printing to incremental SMT2 decision procedure

312c433... by =?utf-8?q?R=C3=A9mi_Delmas?= <email address hidden>

Merge pull request #7083 from remi-delmas-3000/inlining-decoratort-improvements

CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort`

7866f27... by Enrico Steffinlongo <email address hidden>

Merge pull request #7090 from esteffin/esteffin/address-of-array-index

Add address_of(array[index]) support to incremental SMT2 backend

664a7ac... by Remi Delmas <email address hidden>

CONTRACTS: Handle all 4 inlining warning types in `inlining_decoratort`

Modifications:
- move the class from contracts.cpp to its own file
- use regexes to track all 4 types of warnings
- add getter methods to inspect functions involved in warnings
- add methods to throw errors after warnings

4e907dd... by TGWDB <email address hidden>

Merge pull request #7092 from TGWDB/20220901-cbmc-565

Update version number for release 5.65.0

0f7b21c... by Thomas Andrew Spriggs

Add validation for array select argument sorts

381b34d... by Thomas Given-Wilson <email address hidden>

Update version number for release 5.65.0

022f674... by Enrico Steffinlongo <email address hidden>

Add working cbmc-primitives regressions with SMT2