Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002188Frama-CPlug-in > wppublic2015-11-30 12:322015-11-30 12:32
ReporterJochen 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformSodium-20150201OSOS Versionxubuntu14.04
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002188: bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32
DescriptionI ran "frama-c -wp -wp-out wp-out -wp-model Typed+ref -wp-driver jb.drv 484.c" on the attached program (and the attached driver file), and alt-ergo couldn't prove the lemma in line 10-15.

Looking at the background theory in (also attached) file "lemma_l_Alt-Ergo.mlw", it seems that in fact it doesn't imply the goal: axioms about "bit_test" occur only in lines 600 to 819; the only axioms that speak about something different from bit_test in their conclusion are (with line numbers):

 604 axiom bit_test_def1 : relates to bit_testb, which isn't used further
 612 axiom bit_test_extraction1 : relates to land(lsl(1,...))
 622 axiom bit_test_extraction_bis_eq : implies only LSB=1
 701 axiom lsl1_extraction : implies equality of bit position, not of values
 757 axiom to_sint8_extraction_sup : implies negativity, not equality
 773 axiom to_sint16_extraction_sup : similar
 789 axiom to_sint32_extraction_sup : similar
 805 axiom to_sint64_extraction_sup : similar

Axioms about lsl appear only in lines 608 to 1019; axioms speaking about something different from "lsl" and "bit_test" in their conclusion are:

 616 axiom lsl_1_0 : (lsl(1, 0) = 1)
 672 axiom land_1_lsl_1 : is about <, not about =
 833 axiom is_uint8_lsl1_inf : about lsl(1,...) fitting into a uint8
 837 axiom is_uint8_lsl1_sup : about lsl(1,...) not fitting into a uint8
 853 axiom is_uint16_lsl1_inf : similar
 857 axiom is_uint16_lsl1_sup : similar
 873 axiom is_uint32_lsl1_inf : similar
 877 axiom is_uint32_lsl1_sup : similar
 893 axiom is_uint64_lsl1_inf : similar
 897 axiom is_uint64_lsl1_sup : similar
 921 axiom is_sint8_lsl1 : (lsl(1, 7) = 128)
 923 axiom is_sint8_lsl1_inf : about lsl(1,...) fitting into an sint8
 927 axiom is_sint8_lsl1_sup : about lsl(1,...) not fitting into an sint8
 951 axiom is_sint16_lsl1 : (lsl(1, 15) = 32768)
 953 axiom is_sint16_lsl1_inf : similar
 957 axiom is_sint16_lsl1_sup : similar
 981 axiom is_sint32_lsl1 : (lsl(1, 31) = 2147483648)
 983 axiom is_sint32_lsl1_inf : similar
 987 axiom is_sint32_lsl1_sup : similar
1011 axiom is_sint64_lsl1 : (lsl(1, 63) = 9223372036854775808)
1013 axiom is_sint64_lsl1_inf : similar
1017 axiom is_sint64_lsl1_sup : similar

Alltogether, I think there is no way to infer some equality relation from the agreement of bit_test (or land(lsl(...))) results.

I'm not sure whether I used the driver-file mechanism in an appropriate way; this might be the cause for my problem.
TagsNo tags attached.
Attached Filesc file icon 484.c [^] (253 bytes) 2015-11-30 12:32 [Show Content]
? file icon jb.drv [^] (138 bytes) 2015-11-30 12:32
? file icon lemma_l_Alt-Ergo.mlw [^] (40,854 bytes) 2015-11-30 12:32

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-11-30 12:32 Jochen New Issue
2015-11-30 12:32 Jochen Status new => assigned
2015-11-30 12:32 Jochen Assigned To => correnson
2015-11-30 12:32 Jochen File Added: 484.c
2015-11-30 12:32 Jochen File Added: jb.drv
2015-11-30 12:32 Jochen File Added: lemma_l_Alt-Ergo.mlw


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker