From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 50ECC7EE35 for ; Tue, 3 May 2016 17:59:22 +0200 (CEST) IronPort-PHdr: 9a23:oOA/yBfLvH8SIKpsMI7/+7I9lGMj4u6mDksu8pMizoh2WeGdxc6yYR7h7PlgxGXEQZ/co6odzbGG4ua4ASdfu96oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDjvcWLKFoSzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzayXIWSGQbllJzCAjI9hzgFsP+uyHgt+d5njKRPcDsQKocVjGr7qMtQxjt3nQpLTk8pUvQkM1rxJNSoxWroANkwI+cNISRHOt3faTXeswBRmsHWdxeAX8SSrigZpcCWrJSdd1TqJPw8h5X9UOz Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=cppcrazy@gmail.com; spf=Pass smtp.mailfrom=cppcrazy@gmail.com; spf=None smtp.helo=postmaster@mail-wm0-f49.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of cppcrazy@gmail.com) identity=pra; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cppcrazy@gmail.com"; x-sender="cppcrazy@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of cppcrazy@gmail.com designates 74.125.82.49 as permitted sender) identity=mailfrom; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cppcrazy@gmail.com"; x-sender="cppcrazy@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wm0-f49.google.com) identity=helo; client-ip=74.125.82.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="cppcrazy@gmail.com"; x-sender="postmaster@mail-wm0-f49.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0B6AQDryShXjzFSfUpfg1Y1dwYGriqGb4cUhyoHOxEBAQEBAQEBAREBAQEBBwsLCSEvQQ6BXoIVAQEDARIRHQE4AQMBCwEFBQQHNwICIQESAQUBHAYTIodzAwoICZ1xgTE+MYs7hEGHWicNhDsMGAEFCgWKXoJDhHyCWQEEl2UxhXyGJYF3jxJFhwwUhg8SHoEONmGDODowgxaFJgEBAQ X-IPAS-Result: A0B6AQDryShXjzFSfUpfg1Y1dwYGriqGb4cUhyoHOxEBAQEBAQEBAREBAQEBBwsLCSEvQQ6BXoIVAQEDARIRHQE4AQMBCwEFBQQHNwICIQESAQUBHAYTIodzAwoICZ1xgTE+MYs7hEGHWicNhDsMGAEFCgWKXoJDhHyCWQEEl2UxhXyGJYF3jxJFhwwUhg8SHoEONmGDODowgxaFJgEBAQ X-IronPort-AV: E=Sophos;i="5.24,573,1454972400"; d="scan'208,217";a="216821149" Received: from mail-wm0-f49.google.com ([74.125.82.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 May 2016 17:59:21 +0200 Received: by mail-wm0-f49.google.com with SMTP id a17so47672944wme.0; Tue, 03 May 2016 08:59:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc; bh=ys91qXkLCkP4rG1OaO58HY2LezoHdQyUdFUAcHLKgm4=; b=Og0Nbwqj38tev5doFHR00kbakzs4XQDbkF2ZvkKTMjYLbv5D5l3xpdE71CU/gJHNGW EU3wy34TRB33oDJMTN0BzxVFiEZQxkuBgmC7Cnq4JXGuOXfMWz+v486GNBwR1GPhArIg cKocXOH8hYnAa8CLAN0gVqmT7w3jPmKjZR1jgGu12ofKY7VZnJt92zTeM+uh9OKcJTQ4 BvREEn7oHzrPABEOkg+wP/7o9b4cTxMD/UoW31pL5aPVsR8Vj9S1bZ7jSNcL0w/14a2r dRTF86V6HZOr43CM66SfmLL4GkAfXk8BH8slWE+Fh7lUcCqzyzh2sms3YwmlcpiHi8Uk ganA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to:cc; bh=ys91qXkLCkP4rG1OaO58HY2LezoHdQyUdFUAcHLKgm4=; b=iNTWNaXw1j3Kovs7lxla1VQt7PMCAVwCBbzHlCAJL62l27HeQaDTSsI7KsJsfTJ9xi hQOGa6Nk7CGAngUL/vbcovMVJkbXD+iEmMLUWKPbiHSby4BFLgb78rvI7xBvYJXz/LlH V7vtKAAUdFO9rpnapBDc4pql/2t8FiPvPE0R7utICDHBpse8VsSVCr5eTTCTLC0amizk uppO1NKMmSBcO1cWPFPO4l0E6NjxZbE6Hkd8KXHMCda5nQqLFaDamizMwHg44pkQ0fWX vzeyLOjkpXLsywvWvqxPnZotVcCb6++u3wTnuUwMZPGJjPpNM+mk3xBarHwiGuDNY+Uo kQFQ== X-Gm-Message-State: AOPr4FXNcwFngqkNZVLEJ0nfXoJd28+WqbZHSPLdqs2o2JbK7ICc9wp4gpfAlXKO1sbBSACV9GewmuKQID2dQQ== X-Received: by 10.194.231.104 with SMTP id tf8mr3706006wjc.5.1462291161285; Tue, 03 May 2016 08:59:21 -0700 (PDT) MIME-Version: 1.0 Sender: cppcrazy@gmail.com Received: by 10.194.137.84 with HTTP; Tue, 3 May 2016 08:59:01 -0700 (PDT) In-Reply-To: References: <1461935860.9915.100.camel@e130.lan.sumadev.de> <5630123afc948279fc61d5e4c35d9014@in.tum.de> <1461939917.9915.110.camel@e130.lan.sumadev.de> <20160502082756.GC1971@pl-59055.rocqadm.inria.fr> From: Boris Yakobowski Date: Tue, 3 May 2016 17:59:01 +0200 X-Google-Sender-Auth: 53om8_08t5XDvZjI6xJGRV6Z6Ww Message-ID: To: Gabriel Scherer Cc: =?UTF-8?Q?S=C3=A9bastien_Hinderer?= , caml users Content-Type: multipart/alternative; boundary=001a1136369e3a0a860531f23124 Subject: Re: [Caml-list] Obj.out_of_heap_tag, out of minor heap or memory corruption? --001a1136369e3a0a860531f23124 Content-Type: text/plain; charset=UTF-8 On Mon, May 2, 2016 at 4:30 PM, Gabriel Scherer wrote: > I have been trying to motivate the Frama-C people to find an excellent > intern to write a specification of the OCaml memory model in ACSL > (their specification language for C, http://frama-c.com/acsl.html ); > the dream is that one may then be able to use Frama-C to check for > safety of the C stubs, and even possibly verify some parts of the C > codebase in the compiler distribution (probably not the runtime > implementation itself, which precisely breaks the abstraction of the > memory model, but at least large parts of C implementation of > primitives, otherlibs/, etc.). I think they are interested as well, > but I'm not sure they have found the time and people to work on this. > > We're still very much interested in this, although I think the challenges are more important than what you expect. The duality pointer/integer in OCaml's runtime is a major pitfall. Triaging between both by looking at the least significant bit won't be easy to handle. In any case, if somebody looking for an internship is interested by this topic, you're more than welcome to contact me! --001a1136369e3a0a860531f23124 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
On M= on, May 2, 2016 at 4:30 PM, Gabriel Scherer <gabriel.scherer@gma= il.com> wrote:
I have been trying to motivate the Frama-C people to find an excellent
intern to write a specification of the OCaml memory model in ACSL
(their specification language for C, http://frama-c.com/acsl.html );=
the dream is that one may then be able to use Frama-C to check for
safety of the C stubs, and even possibly verify some parts of the C
codebase in the compiler distribution (probably not the runtime
implementation itself, which precisely breaks the abstraction of the
memory model, but at least large parts of C implementation of
primitives, otherlibs/, etc.). I think they are interested as well,
but I'm not sure they have found the time and people to work on this.

We're still very much interested i= n this, although I think the challenges are more important than what you ex= pect. The duality pointer/integer in OCaml's runtime is a major pitfall= . Triaging between both by looking at the least significant bit won't b= e easy to handle.

In any case, if somebody looking for an= internship is interested by this topic, you're more than welcome to co= ntact me!
=C2=A0

--001a1136369e3a0a860531f23124--