-
Notifications
You must be signed in to change notification settings - Fork 13
Open
Description
Running
tri -acsl -dev -arithMode:ilp32 example.cwith content of example.c being
/*@contract@*/
static void f1(int *p)
{
*p = 0;
}
void main()
{
int c;
f1(&c);
}gives
tricera.concurrency.ccreader.CCExceptions$TranslationException: No constructor found to make int a heap object!
at tricera.concurrency.Symex.tricera$concurrency$Symex$$wrapAsHeapObject(Symex.scala:805)
at tricera.concurrency.Symex$PointerDeref.update(Symex.scala:714)
at tricera.concurrency.Symex.evalHelp(Symex.scala:901)
at tricera.concurrency.Symex.eval(Symex.scala:353)
at tricera.concurrency.CCReader$FunctionTranslator.symexFor(CCReader.scala:2337)
at tricera.concurrency.CCReader$FunctionTranslator.translate(CCReader.scala:2489)
at tricera.concurrency.CCReader$FunctionTranslator.translateStmSeq(CCReader.scala:2842)
at tricera.concurrency.CCReader$FunctionTranslator.translate(CCReader.scala:2817)
at tricera.concurrency.CCReader$FunctionTranslator.translateNoReturn(CCReader.scala:2355)
at tricera.concurrency.CCReader.$anonfun$translateProgram$29(CCReader.scala:1065)
at tricera.concurrency.CCReader.$anonfun$translateProgram$29$adapted(CCReader.scala:1036)
at scala.collection.immutable.List.foreach(List.scala:323)
at tricera.concurrency.CCReader.translateProgram(CCReader.scala:1036)
at tricera.concurrency.CCReader.<init>(CCReader.scala:3160)
at tricera.concurrency.CCReader$.apply(CCReader.scala:93)
at tricera.Main.liftedTree1$1(Main.scala:363)
at tricera.Main.run(Main.scala:362)
at tricera.Main$.doMain(Main.scala:122)
at tricera.Main$.main(Main.scala:67)
at tricera.Main.main(Main.scala)
(error "No constructor found to make int a heap object!")
Other Error: No constructor found to make int a heap object!
The expected outcome would be TriCera reporting SAFE
Metadata
Metadata
Assignees
Labels
No labels