Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] State-based contracts in ACSL?

  • Subject: [Frama-c-discuss] State-based contracts in ACSL?
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Sun, 9 Feb 2014 00:24:25 -0500
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C766926AB8@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C766926AB8@Mail1.FCMD.local>
Small correction: please replace "f" by "open".

-----Original Message-----
From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Dharmalingam Ganesan
Sent: Sunday, February 09, 2014 12:19 AM
To: Frama-C public discussion
Subject: [Frama-c-discuss] State-based contracts in ACSL?

Hi,

I have a function 

Bool open(int id);

Informally, f should return true for every new id otherwise returns false.

For example,

open(1) = true; 
open(1) = false;

I read the documentation of ACSL but could not locate anything similar to the above scenario. It seems ghost variables may contribute here(?), but assume we are not allowed to modify the existing definition of f nor we do not have access to any interface to check whether id is already in use .

Any comments?
Dharma

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/avndy0A83hJ5AQsECzBdB4syrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCQvtKetjvW_8Kcfcf6zDHTbFFzxT9I9LCzBxfBHEShhlLtzBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdIcec6PiSbNRniZyW4GmrFgQKCy0oDI_bAdFW1EwJm4UXqt3h1a1Ew418o2F8SMYr75XFvb1Qw1U