--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on October 2020 ---
Hello, I am working with the definitions of limits in frama-c. In Coq, limits have been defined using the filters in the Coquelicot library. I used this definition in my Coq proof. I am trying to define limits in ACSL/Frama-C to verify certain properties of C modules. Is there a way to directly use the filter definition of limits from Coquelicot in ACSL/Frama-C ? Or would you suggest that I define the limits in ACSL separately and prove the equivalence in Coq ? Thanking you, Mohit Tekriwal -- Mohit Tekriwal, PhD Candidate, Department of Aerospace Engineering, University of Michigan. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20201005/face7d32/attachment.html>