Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002087Frama-CPlug-in > wppublic2015-03-03 21:412015-03-09 10:06
ReporterIan 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSUbuntuOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0002087: Able to assert a false statement
DescriptionIn the attached program, 'absurd' validates when it should not. The is only observed when all of the following conditions are met. 'num' must be part of a struct, which can be global (as in the program below) or returned from split. Changing the assigns to only r.num cause the correct behavior. However, if the struct is returned from split, absurd still validates. 'split' must be called, if the body is inlined, the bad behavior is not observed. Alt-ergo 0.99.1 must be used, can not replicate using 0.95.2 The expression must be '5/2', I have not found any other numbers that causes this behavior.
Steps To ReproduceCreate struc_div.c (attached): struct result { int num; }; struct result r; /*@ assigns r; ensures r.num == 5/2; */ void split() { r.num = 5/2; } void test_split() { split(); //@ assert absurd: r.num == -99 && r.num == 99; } Run: frama-c struct_div.c -wp -wp-rte Results: [kernel] preprocessing with "gcc -C -E -I. struct_div.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function split [rte] annotating function test_split [wp] 3 goals scheduled [wp] [Qed] Goal typed_split_post : Valid [wp] [Qed] Goal typed_split_assign : Valid [wp] [Alt-Ergo] Goal typed_test_split_assert_absurd : Valid (26ms) (18) [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 (26ms-26ms) (18) Expected that 'absurd' assertion should not validate.
TagsNo tags attached.
Attached Filesc file icon struct_div.c [^] (236 bytes) 2015-03-03 21:41 [Show Content]
? file icon foo.mlw [^] (379 bytes) 2015-03-05 13:30

- Relationships

-  Notes
(0005803)
correnson (manager)
2015-03-09 10:06

After reducing the bug to a minimal version, this is due to an Alt-Ergo bug. https://github.com/OCamlPro/alt-ergo/issues/10

- Issue History
Date Modified Username Field Change
2015-03-03 21:41 Ian New Issue
2015-03-03 21:41 Ian Status new => assigned
2015-03-03 21:41 Ian Assigned To => correnson
2015-03-03 21:41 Ian File Added: struct_div.c
2015-03-05 13:30 bobot File Added: foo.mlw
2015-03-09 10:06 correnson Note Added: 0005803
2015-03-09 10:06 correnson Status assigned => acknowledged


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker