cbmc:smt2-float-conversions

Branch merges

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related charm recipes

bea0345... by Daniel Kroening <email address hidden> on 2019-01-01

smt2: fix the casts from c_bit_field to floatbv

97759a3... by Daniel Kroening <email address hidden> on 2019-01-01

floatbv can now do floatbv_typecast from c_bit_field

37a8720... by Michael Tautschnig on 2018-12-31

Merge pull request #3646 from diffblue/smt2-tag-types

SMT2: convert struct_tag and union_tag types

d11ec53... by Michael Tautschnig on 2018-12-31

Merge pull request #3624 from tautschnig/vs-knownbug

Mark failing tests KNOWNBUG [blocks: #2310, #3627]

170c522... by Daniel Kroening <email address hidden> on 2018-12-28

smt2: convert struct_tag and union_tag types

The SMT2 backend can now convert struct_tag and union_tag types. This will
enable a future change whereby these types are no longer expanded by the
program analyzer.

786f797... by Michael Tautschnig on 2018-12-29

Merge pull request #3640 from diffblue/smt2-bound-symbols

smt2: fix exists/forall

9f1aa87... by Michael Tautschnig on 2018-12-29

Merge pull request #3639 from diffblue/smt2-with-full-size

smt2: fix encoding of with expressions

a3fe0f8... by Michael Tautschnig <email address hidden> on 2018-12-28

Mark tests failing on Windows as KNOWNBUG

All 35 fail with

File: arith_tools.cpp:196 function: from_integer
Condition: false
Reason: Precondition

a122ff4... by Michael Tautschnig <email address hidden> on 2018-12-28

The first static_assert fails with goto-cl

The regression test is not run on Windows due to earlier failures.

fa63ef1... by Michael Tautschnig <email address hidden> on 2018-12-28

goto-cl does not print source lines

The regression was not running on Windows because of earlier failures.