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] \at in ACSL assertions

  • Subject: [Frama-c-discuss] \at in ACSL assertions
  • From: jorge.honoratpoblette at enseeiht.fr (Jorge Luis Honorat Poblette)
  • Date: Wed, 08 Dec 2010 18:11:21 +0100
  • In-reply-to: <AANLkTimyk_961c8Xk6_U33TAxabBGSeoaRB+EtM-OiBR@mail.gmail.com>
  • References: <AANLkTimyk_961c8Xk6_U33TAxabBGSeoaRB+EtM-OiBR@mail.gmail.com>
Hello Pascal im working with abstract interpretation and weakest 
precondition analysis, I saw your email info on the mailing list of 
frama-c and I would like to ask you if maybe you know if C constructs  
as loops and "ifs" structures can be splited to generate this anlysis, 
any reference will be helpfull, best regards.

-- 
Jorge Luis Honorat
Mail : jorge.honoratpoblette at enseeiht.fr

IRIT - ENSEEIHT
DSI INP Toulouse
bureau E118
2 rue Charles Camichel - 31071 TOULOUSE Cedex 7