Size axioms for struct constants causing inconsistencies

[zvonimir]

Problematic example is examples/svcomp/ntdrivers/floppy_unsafe.i.cil.c.
I've been working off the cleaning-alloc branch.

Using twodim, these are the two problematic axioms that get generated:
axiom ($size($obj($pa($ptr(MOUNTDEV_MOUNTED_DEVICE_GUID, 0), 12, 1))) == 8);
axiom ($size($obj($pa($ptr(MOUNTDEV_MOUNTED_DEVICE_GUID, 0), 20, 1))) == 4);

Flat model has the same problems and the axioms there are also wrong, but not inconsistent.

[zvonimir]

Ok, root cause is in SmackRep::addInit. While initialization is by its nature recursive, setting $size is not since $size should be set only for the whole object.
One question that I have is why do we even need these lines:
program->addDecl(
Decl::axiom(
Expr::eq(
Expr::fn("$size", ptr2ref(addr)),
lit(at->getNumElements()) )));
Since $size is not being set for any other type of objects anyways.

[michael-emmi]

Well I have ruled out your root cause in commit 861dd6e by completely removing the $size predicate (which is practically useless), yet the following

smack-verify.py floppy_unsafe.i.cil.bc --mem-mod=twodim

still does not report the violation which is reported with --mem-mod=flat.

...so the investigation continues. :-)

[zvonimir]

The problem mentioned in the previous comment was caused by unsound handling of ptr2int in the twodim memory model, which is being phased out. So I am closing this issue.