Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma

Benutzer


products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Isabelle_C/ Datei vom 31.4.2026 mit Größe 6 kB

Quelle README.thy

Sprache: Isabelle

(******************************************************************************
* Isabelle/C
*
* Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
*     * Redistributions of source code must retain the above copyright
*       notice, this list of conditions and the following disclaimer.
*
*     * Redistributions in binary form must reproduce the above
*       copyright notice, this list of conditions and the following
*       disclaimer in the documentation and/or other materials provided
*       with the distribution.
*
*     * Neither the name of the copyright holders nor the names of its
*       contributors may be used to endorse or promote products derived
*       from this software without specific prior written permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
* "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
* LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
* A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
* OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
* DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
* THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
******************************************************************************)

(* Authors: Frédéric Tuong, Burkhart Wolff *)

theory README imports Main begin

section ‹Isabelle/C›

text ‹
/C contains a C99/C11/C18 front-end support for Isabelle. The front-end is actually composed
two possibly interchangeable parsers (from two different projects):

▪ 🍋‹C11-FrontEnd›: 🪙‹https://hackage.haskell.org/package/language-c›
▪ 🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C18-FrontEnd›:
🪙‹https://github.com/jhjourdan/C11parser›

present, the recommended and default version is C11.
›

section ‹Getting started›

text ‹ A first installation step is:
▪ 🍋‹isabelle build -D› 🍋‹.›
›
text ‹ which should work out of the box.
›

text ‹ The following C examples or entry-points of documentation can be executed:

▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C0.thy›
▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C2.thy›
▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/examples/C1.thy›
▪ 🍋‹isabelle jedit -d› 🍋‹.› 🍋‹C11-FrontEnd/appendices/C_Appendices.thy›
›

text ‹
▪ The example 🍋‹C11-FrontEnd/examples/C0.thy› is basically used to
the faithfulness of the C11 parser implementation.
▪ The example 🍋‹C11-FrontEnd/examples/C2.thy› shows common cases of C and
editing support in PIDE; it also contains annotation commands without any semantics.
▪ The example 🍋‹C11-FrontEnd/examples/C1.thy› is a show-case for markup
and the use of bindings resulting from the static C environment.
▪ The example 🍋‹C11-FrontEnd/appendices/C_Appendices.thy› shows the use of
/C documentation facilities.
›

text ‹
AFP version of Isabelle/C does not include semantic back-ends (these are distributed by other
submissions or available via the web; see below). The structure of 🍋‹.› has
designed to create a directory ‹C11-BackEnds› into which back-ends can be
. The structure of 🍋‹.› is actually similar as
🪙‹https://gitlri.lri.fr/ftuong/isabelle_c›: see for example
🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C11-BackEnds› where several
-ends can be copied and tried.
›

subsection ‹Isabelle/C/README›

text ‹
🍋‹README.md› is automatically generated from 🍋‹README.thy›
🪙‹https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/README.sh›.
›

text ‹ Note that this shell-script requires the prior installation of
🍋‹pandoc› (🪙‹https://github.com/jgm/pandoc›).
›

section ‹Authors›

text ‹
▪ Frédéric Tuong (🪙‹https://www.lri.fr/~ftuong›)
▪ Burkhart Wolff (🪙‹https://www.lri.fr/~wolff›)
›

section ‹License›

text ‹
/C is licensed under a 3-clause BSD-style license (where certain files are in the HPND
compatible with the 3-clause BSD).

more details:
▪ The generated files 🍋‹C11-FrontEnd/generated/c_ast.ML› and
🍋‹C11-FrontEnd/generated/c_grammar_fun.grm› are mixing several source code of
different projects:
▪ In 3-clause BSD: the part representing the Haskell Language.C library.
▪ In 2-clause BSD: the C99 AST in HOL (before reflection to SML) adapted from the original
one in the L4.verified project.
▪ In 3-clause BSD: the HOL translation C11 to C99 from the Securify project.
▪ In 3-clause BSD: any other binding and translations of meta-models from the Citadelle
project.
▪ In 3-clause BSD: the two combined generators generating
🍋‹C11-FrontEnd/generated/c_ast.ML› based on some modified version of Haskabelle
and Citadelle.
▪ In 3-clause BSD: the Happy modified generator generating
🍋‹C11-FrontEnd/generated/c_grammar_fun.grm›
▪ In HPND: the ML-Yacc modified generator generating the two
🍋‹C11-FrontEnd/generated/c_grammar_fun.grm.sig› and
🍋‹C11-FrontEnd/generated/c_grammar_fun.grm.sml› (i.e., the ML-Yacc version of
MLton).
▪ In HPND: the modified grammar library of ML-Yacc loaded in
🍋‹C11-FrontEnd/src/C_Parser_Language.thy›.
▪ In 3-clause BSD: the remaining files in 🍋‹C11-FrontEnd/src› constituting
Isabelle/C core implementation.
▪ Most examples in 🍋‹C11-FrontEnd/examples› are in 3-clause BSD, some are
used for quotation purposes to test the Isabelle/C lexer (hyperlinks around each example detail
their provenance).
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.7 Sekunden ¤

Wurzel

Suchen

NIST Cobol Testsuite

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.