0001767: Problem when arguments are not used in predicates

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001767

Frama-C

Plug-in > wp

public

2014-04-30 10:07

2015-03-17 22:17

Reporter

davyg

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Neon-20140301

Target Version

Fixed in Version

Frama-C Sodium

Summary

0001767: Problem when arguments are not used in predicates

Description

The following example generates an error when it is exported to coq/why3 or alt-ergo.

/*@predicate p(double x, int y) = y;*/

/*@lemma lem : p((double) 0, (int) 1);*/

The why file generated by wp is the following one :

theory Axiomatic

...

predicate p_p (y_0 : int) = 0 <> y_0

lemma Q_lem: (p_p 1.0)

end

Wp detects that x is not used so it does not appear in why predicate p_p when it is used in Q_lem the correct value is taken(1) but its type is incorrect that's why wp put 1.0(a real) and not 1(an int) as argument. It takes the correct value : the one of the second argument in the original lemma but takes the type of the first argument to generate the constant and not the second one.

Steps To Reproduce

Write a file test.c with :

/*@predicate p(double x, int y) = y;*/

/*@lemma lem : p((double) 0, (int) 1);*/

And run frama-c -wp test.c

You will get the following error :

[kernel] preprocessing with "gcc -C -E -I. test.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
/tmp/wpd136d4.dir/typed/lemma_lem.ergo:9:[wp] user error: Alt-Ergo error:
                 characters 17-25:typing error: int and real cannot be unified
[wp] [Alt-Ergo] Goal typed_lemma_lem : Failed
     Error: characters 17-25:typing error: int and real cannot be unified
[wp] Proved goals: 0 / 1
     Alt-Ergo: 0 (failed: 1)

Tags

No tags attached.

Attached Files

Relationships

Notes
(0005190) correnson (manager) 2014-06-02 17:42	Fix committed to master branch.

Issue History
Date Modified	Username	Field	Change
2014-04-30 10:07	davyg	New Issue
2014-04-30 10:07	davyg	Status	new => assigned
2014-04-30 10:07	davyg	Assigned To	=> correnson
2014-06-02 17:42	correnson	Note Added: 0005190
2014-06-02 17:42	correnson	Status	assigned => resolved
2014-06-02 17:42	correnson	Resolution	open => fixed
2015-03-17 22:17	signoles	Fixed in Version	=> Frama-C Sodium
2015-03-17 22:17	signoles	Status	resolved => closed