Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #579

Closed
Open
Created Nov 30, 2015 by Jochen Burghardt@burghardt

bit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32

ID0002188: This issue was created automatically from Mantis Issue 2188. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002188 Frama-C Plug-in > wp public 2015-11-30 2015-11-30
Reporter Jochen Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform Sodium-20150201 OS - OS Version xubuntu14.04
Product Version Frama-C Sodium Target Version - Fixed in Version -

Description :

I 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.

Attachments

  • 484.c
  • jb.drv
  • lemma_l_Alt-Ergo.mlw
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking