coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Lessness Randomness <lessnessr AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] [Newbie question about CompCert]
Date: Tue, 9 Jan 2018 22:21:15 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lessnessr AT gmail.com; spf=Pass smtp.mailfrom=lessnessr AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f47.google.com
Ironport-phdr: 9a23:m04csRfjlK5HMNMkDOt+RAYqlGMj4u6mDksu8pMizoh2WeGdxcqzbR7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5u6YYQRFOoBJuBYoJfmp1sVsBCwGROjBOXyxT9Pg3/227M10/86EQrb2wEgG8wBsG/PrNXzKqgSSvu1zLPTwDXMavNZwzb96IzSfh89pvGMWKt9fMzMwkcsDwPIlledpIP/Mz+IyOgAs3KX4ul+We61hGMqqQd8qSW1yMg2kInGnIcVx0jE9SpnxIY1IsW1SEthbt6lFJtcri+bN45qTs87TWFltyQ3xqcJuZ68eygKx5AnyADFZ/ObdIiI5wrvVOeXIThmmHJoYLCyihmo/US91OHxVtO43VVUoiZfndTBtGgB1xnJ5ciGTvt98F2h2TGK1w3L7uFLP1s0lbHdK5E/2b4wjYATvF/MHi/zgkr2jauWel849eiv7uTreq/mqYOEN49olgH+NbwjldC4AeQhKwQBQ2yb+fmn27D45k34QLBKjuUsnaXDsZDaI94bpq+jDANP3IYj8UX3MzDz29MB2HIDMVhteRSdjoGvNUudDur/CKKbjk+3ljpw3Lj8N7vtBZDLI2PY2OPlcK1m7UNH0xAbwtVW5pYSAbYEdqGgEnTtvcDVW0dqeze/xPzqXY1w

Hello,

Is it possible (using CompCert library in Coq, its formalisation of the C) to specify and prove properties of C functions?

(As far I know, it's only possible to compile a whole program (with main()). Maybe I'm mistaken.)

[Coq-Club] [Newbie question about CompCert], Lessness Randomness, 01/09/2018
- Re: [Coq-Club] [Newbie question about CompCert], Li-yao Xia, 01/09/2018
  - Re: [Coq-Club] [Newbie question about CompCert], Lessness Randomness, 01/09/2018