0002497: quantifiers over logic types do not restrict to valid instances

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002497

Frama-C

Plug-in > wp

public

2020-01-30 19:40

2020-02-03 11:39

Reporter

amosr

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Product Version

Frama-C 20-Calcium

Target Version

Fixed in Version

Summary

0002497: quantifiers over logic types do not restrict to valid instances

Description

Hi,

When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:

> //@ type logic_type_with_u8 = value(unsigned char);

This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, `\forall logic_type_with_u8 l` has to prove that the predicate is true even for values that won't fit in a u8.

As a concrete example, I expect the following to hold, but it does not:

> lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);

Thanks,
Amos

Steps To Reproduce

Download file logic_type_is_valid.c and run with WP:

> frama-c -wp logic_type_is_valid.c

The lemma in this file should hold, but does not.

Additional Information

PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?

Tags

No tags attached.

Attached Files

logic_type_is_valid.c (167 bytes) 2020-01-30 19:40

/*@
  type logic_type_with_u8
    = value(unsigned char);

  lemma u8_is_valid:
    \forall logic_type_with_u8 n;
    \exists unsigned char u;
      n == value(u);
*/

logic_type_is_valid.c (167 bytes) 2020-01-30 19:40

Relationships

Relationships

Notes
~0006934 amosr (reporter) 2020-01-30 19:48	From what I can tell, this is only incomplete rather than unsound – I can't figure out a way to prove "there exists some logic_type_with_u8 such that its u8 is 256".

~0006935 correnson (manager) 2020-02-03 11:39	Yes indeed, you are right, there _is_ something missing here. And I'm afraid this can lead to soundness issues, at least regarding ACSL expected semantics.

Notes

Date Modified	Username	Field	Change
Issue History
2020-01-30 19:40	amosr	New Issue
2020-01-30 19:40	amosr	Status	new => assigned
2020-01-30 19:40	amosr	Assigned To	=> correnson
2020-01-30 19:40	amosr	File Added: logic_type_is_valid.c
2020-01-30 19:48	amosr	Note Added: 0006934
2020-02-03 11:39	correnson	Note Added: 0006935

Issue History