From 73fa920959d22c084265fe847f4788564bf49700 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 7 May 2014 16:13:31 +0200 Subject: Achieve nothing. --- Makefile | 6 +- abstract/constant_domain.ml | 155 +++++++++++++++++++++++++++++++--- abstract/domain.ml | 7 ++ doc/TP1.html | 185 +++++++++++++++++++++++++++++++++++++++++ doc/TP1_files/main.js | 126 ++++++++++++++++++++++++++++ doc/TP1_files/preferred.css | 23 +++++ doc/enonce.html | 170 +++++++++++++++++++++++++++++++++++++ doc/enonce_files/main.js | 126 ++++++++++++++++++++++++++++ doc/enonce_files/preferred.css | 23 +++++ libs/util.ml | 8 ++ main.ml | 11 ++- 11 files changed, 825 insertions(+), 15 deletions(-) create mode 100644 doc/TP1.html create mode 100644 doc/TP1_files/main.js create mode 100644 doc/TP1_files/preferred.css create mode 100644 doc/enonce.html create mode 100644 doc/enonce_files/main.js create mode 100644 doc/enonce_files/preferred.css create mode 100644 libs/util.ml diff --git a/Makefile b/Makefile index 640da3b..0f09d87 100644 --- a/Makefile +++ b/Makefile @@ -1,12 +1,12 @@ .PHONY: clean BIN=analyze -SRCDIRS=libs,frontend +SRCDIRS=libs,frontend,abstract all: $(BIN) -$(BIN): main.ml - ocamlbuild -Is $(SRCDIRS) main.native +$(BIN): main.ml abstract/domain.ml abstract/constant_domain.ml + ocamlbuild -Is $(SRCDIRS) -cflags '-I /usr/lib/ocaml/zarith' -lflags '-I /usr/lib/ocaml/zarith zarith.cmxa' main.native mv main.native $(BIN) clean: diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index 8444779..544d2e9 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -1,18 +1,153 @@ +open Util +open Abstract_syntax_tree - -module Make : Domain.s = +module CD : Domain.S = struct + exception DivideByZero + exception TypeError + exception Bot + exception NotImplemented - type tv = - | Bot - | BTrue - | BFalse - | BTop - | I of Z.t - | ITop + type tv = (* type for a variable *) | Top + | I of Z.t + + type ts = (* type for an environment *) + | Bot + | Nb of tv VarMap.t + + let top_ts = Nb VarMap.empty - type ts = tv VarMap.t + let ts_union a b = + begin match a, b with + | Bot, Bot -> Bot + | Nb a, Bot -> Nb a + | Bot, Nb b -> Nb b + | Nb a, Nb b -> + Nb + (VarMap.fold + (fun var value a -> + try match VarMap.find var a with + | Top -> a + | I x -> + match value with + | I y when y = x -> a + | _ -> VarMap.add var Top a + with + | Not_found -> VarMap.add var value a) + b a) + end + + (* must not raise exception *) + let ts_add_bool_constraint expr (s : ts) = + s (* TODO, not necessary... *) + + + (* only evaluates numerical statements, raises + TypeError when result is bool *) + let rec eval_abs expr (s : tv VarMap.t) = + match expr with + | AST_unary(op, (i, _)) -> + begin match eval_abs i s with + | Top -> Top + | I x -> + match op with + | AST_UNARY_PLUS -> I x + | AST_UNARY_MINUS -> I (Z.neg x) + | _ -> raise TypeError + end + | AST_binary(op, (a, _), (b, _)) -> + begin match eval_abs a s, eval_abs b s with + | I x, I y -> + begin match op with + | AST_PLUS -> I (Z.add x y) + | AST_MINUS -> I (Z.sub x y) + | AST_MULTIPLY -> I (Z.mul x y) + | AST_DIVIDE -> + if y = Z.zero then raise DivideByZero; + I (Z.div x y) + | AST_MODULO -> + if y = Z.zero then raise DivideByZero; + I (Z.rem x y) + | _ -> raise TypeError + end + | _ -> Top + end + | AST_identifier(id, _) -> + begin + try VarMap.find id s + with _ -> Top + end + | AST_int_const(s, _) -> + I (Z.of_string s) + | AST_bool_const(_) -> raise TypeError + | AST_int_rand _ -> Top + | _ -> raise NotImplemented (* extensions *) + + (* returns true if the expression can evaluate to true + returns false if the expression always evaluates to false *) + let rec eval_bool_abs expr (s : tv VarMap.t) = + true (* TODO *) + + (* must not raise exception *) + let rec interp_abs stat s = + begin match s with + | Bot -> Bot + | Nb vars -> + begin match stat with + | AST_block b -> + List.fold_left + (fun ss (st, _) -> interp_abs st ss) + s b + | AST_assign ((id, _), (exp, _)) -> + begin + try + let value = eval_abs exp vars in + Nb (VarMap.add id value vars) + with _ -> Bot + end + | AST_if ((cond, _), (tb, _), None) -> + ts_union (Nb vars) + (interp_abs tb + (ts_add_bool_constraint cond (Nb vars))) + | AST_if ((cond, l), (tb, _), Some (eb, _)) -> + ts_union + (interp_abs tb + (ts_add_bool_constraint cond (Nb vars))) + (interp_abs eb + (ts_add_bool_constraint + (AST_unary (AST_NOT, (cond, l))) + (Nb vars))) + | AST_while ((cond, _), (body, _)) -> + let f s = + ts_union + s + (ts_add_bool_constraint cond s) + in + fix f (Nb vars) + | AST_HALT -> Bot + | AST_assert (cond, _) -> + if eval_bool_abs cond vars + then Nb vars + else begin + print_string "Assert fail\n"; + Bot + end + | AST_print items -> + List.iter + (fun (var, _) -> + print_string (var ^ " = "); + try + match VarMap.find var vars with + | Top -> print_string "T\n" + | I x -> print_string (Z.to_string x ^ "\n") + with _ -> print_string "T\n") + items; + Nb vars + | _ -> raise NotImplemented (* extensions *) + end + end end + diff --git a/abstract/domain.ml b/abstract/domain.ml index d022e34..643a6ec 100644 --- a/abstract/domain.ml +++ b/abstract/domain.ml @@ -1,7 +1,14 @@ +open Abstract_syntax_tree module type S = sig type tv type ts + + val top_ts : ts + + val interp_abs : stat -> ts -> ts end + + diff --git a/doc/TP1.html b/doc/TP1.html new file mode 100644 index 0000000..dfb8def --- /dev/null +++ b/doc/TP1.html @@ -0,0 +1,185 @@ + + +Semantics and application to program verification, École normale supérieure, 2013-2014 + + + + + + + +

Semantics and application to program verification

+ +
+ +

TP1 - Denotational semantics

+ +

+The goal of this session is to program an interpreter to compute the denotational semantics of a simple language. +We will use OCaml. + + +

Language

+ +

+Start by downloading the package: codeV1.tgz. + +

+The package contains a parser for the language, programmed in OCamlLex and Menhir (lexer.mll and parser.mly). +The parser outputs an abstract syntax tree defined in abstract_syntax_tree.ml. +A pretty-printer, to print back an abstract syntax tree into the original language, is provided in abstract_syntax_printer.ml. +In main.ml, you will find a simple driver that takes a file name passed as argument, parses it, and prints it back. +Just typing make should compile the simple driver. + +

Syntax

+

+The language is a very simple "curly brackets" C-like language. +A program is composed of a sequence of statements of the form: +

+

+non-standard statements include: +

+ +

+Expressions include: integer arithmetic operators: +, -, *, /, % (modulo); boolean operators: && (and), || (or), ! (negation); integer comparisons <, <=, >, >=. +Equality == and disequality != can be used to compare either two integers or two boolean values. +Constants include integers, and the boolean constants true and false. +Finally, rand(l,h) denotes the non-deterministic interval of integers between the constant l and the constant h. +You can use /* ... */ and // comments. +You can use parentheses and the operators have their usual precedence. + +

+Unlike C, variables do not need to be declared; they start existing when first assigned a value. +There are no local variables nor functions (see the extension part). + +

Semantics

+ +

+Variables have no type and can hold either an integer or a boolean +value. +Subsequently, we do not distinguish statically between boolean and +integer expressions: only values have a type. +It is an error to use operators with values of the wrong type, such as +adding two boolean values. +This is detected at run-time, when evaluating the expression in the +current environment. +Other run-time errors include: divisions and modulos by zero; using a +non-boolean value in tests, loops and assert conditions; using a +variable that has never been assigned to; asserting a condition that is +false; executing the halt statement. + + +

Deterministic semantics

+ +

+We first consider the deterministic subset of the language, i.e., we ignore the AST_int_rand expression node for now. + +

+Write an interpreter that executes the program by induction on the +syntax of statements and expressions; it returns either an environment +mapping variables to values, or an error. + +

+You can use the following steps: +

    +
  1. Define a type ival for values. It should contain integers, + booleans and errors. +You can use a string representation for errors, which will give the user + some information on the location and cause of the error. +To avoid possible overflow in arithmetic, you can use the ZArith OCaml library (its API is similar to that of Int32 and Int64; the module is called Z). +
  2. Define a type env for environments. You can use the Map + functor from the standard OCaml library to represent mappings from +variables to (non-erroneous) values. In addition to such mappings, an env object can also represent an error. The initial environment is an empty map (no variable). +
  3. Write an expression evaluation function eval_expr: env -> expr ext -> ival by induction on the syntax of expressions. +It returns an error if its env argument is an error +(strictness) or if an error is detected in the expression evaluation, +which then percolates to the expression root. +Avoid using OCaml exceptions to propagate errors in the function: it +will only make the construction of the non-deterministic version more +painful! +
  4. Write a statement evaluation function eval_stat: env -> stat ext -> env. +When should the function return an error environment? +
  5. +Test your interpreter on the programs from the examples directory. +Can you detect infinite loops in loop.c, loop2.c, and loop3.c? +Under which condition does your interpreter terminate? +
+ +

+new: correction available in interp_det.ml. +(The correction uses abstract syntax trees from the extended language in codeV1x.tgz) + +

Non-deterministic semantics

+ +

+We now consider the full language including the non-deterministic expression node rand(l,h). + +

+Write an interpreter for this language that outputs the set of all +possible environments at the end of the program as well as the set of +all errors that can be encountered. + +

+The structure of the interpreter will be similar to the one in the previous question. +You can use the following steps: +

    +
  1. Define a type ivalset to represent sets of values ival (including errors). +You can use OCaml's standard Set functor. +
  2. Define a type envset to represent sets of environments (including errors). +
  3. Program a function eval_expr: env -> expr ext -> ivalset + to evaluate an expression in a single environment and return the set of + its possible values in the environment. +When encountering a unary node, the operator must be applied to each +possible value of its argument expression; you can use iterators such as + fold. +Binary nodes require nested fold. +
  4. Program a filter function filter: envset -> expr ext -> envset that returns the subset of its envset argument that can satisfy the expression, enriched with the errors encountered during the expression evaluation. +This function will be useful to model loops, tests and assertions. +Remember that an environment can satisfy both an expression and its negation! +
  5. Program a generic fixpoint operator fix: ('a -> 'a) -> 'a -> 'a that iterates a function from a base element to reach a fixpoint. +Use it then in the semantics of loops. +
  6. +Test your interpreter on the examples directory, including non-deterministic programs such as gcd_nd.c and loop4.c. +
+ +

+new: correction available in interp_ndet.ml. +(The correction uses abstract syntax trees from the extended language in codeV1x.tgz) + + + +

Extensions

+ +

+You will find in codeV1x.tgz + an extension of the language with the following additional constructs: +variable declarations (global and local), procedures and functions, break and return statements, labels and goto + statements. +The language is completely backward compatible with the simpler one. +The abstract syntax tree also enriches the previous one with new kinds +of nodes, so that you can simply reuse your interpreter and extend it to + support some or all of the new constructs. + +

+

+
+

+Author: Antoine Miné +

+ + +

+ + + + + \ No newline at end of file diff --git a/doc/TP1_files/main.js b/doc/TP1_files/main.js new file mode 100644 index 0000000..a1e13a0 --- /dev/null +++ b/doc/TP1_files/main.js @@ -0,0 +1,126 @@ +/* + Scripts for my professional web-site: http://www.di.ens.fr/~mine + Copyright (C) Antoine Miné 2011. + */ + + +/* main menu */ +var options = [ + ["img", "antoine_mini.png", "80%", "" ], + ["Antoine Miné", "", "", "" ], + ["br"], + ["Home", "Accueil", "index", "" ], + ["News", "Nouvelles", "index", "#news" ], + ["Research", "Recherche", "index", "#research" ], + ["Habilitation", "Habilitation", "hdr/index", "", "" ], + ["Ph.D", "Thèse", "these/index", "" ], + ["Projects", "Projets", "projects", "" ], + ["Conferences", "Conférences", "confs", "", ], + ["Software", "Logiciels", "index", "#soft", ], + ["Publications", "Publications", "publications", "", "important" ], + ["Talks", "Exposés", "talks", "" ], + ["Teaching", "Enseignement", "index", "#teach", ], + ["Emulation", "Émulation", "emulation", "" ], + ["Contact", "Contact", "index", "#contact" ], + ["-"], +/* + ["SAS 2012", "", "http://www.sas2012.ens.fr", "", "important" ], + ["SSCPS 2012", "", "http://www.sscps.net", ""], + ["SAS 2013", "", "http://research.microsoft.com/en-us/events/sas2013/", ""], +*/ + ["iFM 2014", "", "http://ifm2014.cs.unibo.it/", ""], + ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""], + ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""], + ["TASE 2014", "", "http://www.nudt.edu.cn/tase2014", ""], + ["POPL 2015", "", "http://popl.mpi-sws.org/2015/", ""], + ["-"], + + ["MPRI 2-6 course (M2)", "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""], + ["Semantic course (L3)", "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""], + + ["-"], + ["AstréeA", "", "http://www.astreea.ens.fr", "", "important" ], + ["Astrée", "", "http://www.astree.ens.fr", "" ], + ["Apron", "", "http://apron.cri.ensmp.fr/library", "" ], + ["-"], + ["br"], + ["img", "logo-cnrs.png", "64", "http://www.cnrs.fr" ], + ["br"], + ["img", "logo-ens.png", "82", "http://www.ens.fr" ], + ["br"], + ["img", "logo-inria.png", "128", "http://www.inria.fr" ], +]; + +function print_menu(base,here) +{ + for (var i=0; i\n"); + + else if (options[i][0] == "br") + document.write("
\n"); + + else if (options[i][0] == "img") { + document.write("
"); + if (options[i][3] != "") + document.write(""); + document.write("\"[""); + if (options[i][3] != "") + document.write(""); + document.write("
\n"); + } + + else { + document.write("
"); + var url = options[i][2]; + if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3]; + if (url != "" && url.indexOf(":") == -1) url = base + url; + if (options[i][0] == here || url=="") document.write(""); + else if (4 in options[i]) document.write(""); + else document.write(""); + document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]); + if (options[i][0] == here || url=="") document.write(""); + else document.write(""); + document.write("
\n"); + } + } +} + +function print_ref(s) +{ + document.write(""); + document.write("[" + s + "]"); + document.write(""); +} + +function mailchar(m,i) +{ + var c = ""; + switch (i) { + case 0: c = 'm'; break; + case 1: c = 'i'; break; + case 2: c = 'n'; break; + case 3: c = 'e'; break; + case 4: c = '@'; break; + case 5: c = 'd'; break; + case 6: c = 'i'; break; + case 7: c = '.'; break; + case 8: c = 'e'; break; + case 9: c = 'n'; break; + case 10: c = 's'; break; + case 11: c = '.'; break; + case 12: c = 'f'; break; + case 13: c = 'r'; break; + } + if (c != "") m.innerHTML = m.innerHTML + "" + c + ""; + if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random()); +} + +function main() +{ + var m = document.getElementsByName("mail"); + for (var i=0; i + +Semantics and application to program verification, École normale supérieure, 2013-2014 + + + + + + + +

Semantics and application to program verification

+ +
+ +

Project

+ +

+The goal of the project is to write a simple static analyzer by abstract + interpretation in OCaml to discover automatically numeric invariants +about the variables of programs written in a simple programming +language. + +

+The project is due on the day of the exam, on May the 28th. +The project should be sent by email to the teachers. + +

Result

+ +

+For the project, you should deliver an archive that contains the following items: +

    +
  • the source code of the static analyzer, well-commented and complete with a Makefile; +
  • a report of 4 pages or more that describes the language +features supported, the choices in semantics and implementation (if +any), the usage of the analyzer; it must also discuss the result of a +few analysis tests (we provide some tests that you can use). +
+ + +

Required features

+ +

Input language

+ +

+The input language can be based on the language used in the lab session, + or you can design your own language with similar features. +To get started, you can download the codeV1x.tgz package (see the first practical session for an explanation of the syntax of the language). + +

+More precisely, the language must feature at least: +

    +
  • blocks (nested sequences of instructions); +
  • declarations of variables of integer type, with proper scoping with respect to blocks (to simplify, you can assume that all variable names are distinct); +
  • assignments of integer expressions, with the standard arithmetic operators: +, -, * (and optionally division / and modulo %); +
  • if-then-else instructions, using boolean expressions containing integer comparisons (==, !=, <, >, <=, >=) and boolean operators (&&, ||, !) (support for boolean variables is not required); +
  • while loops; +
  • a non-deterministic operation, such as rand(l,h) in integer expressions; +
  • an assert instruction, that checks the validity of a boolean expression; +
  • a print instruction, that takes as argument a list of variables and prints their value. +
+ +

+(You are free to reject programs using other language +constructions, such as functions, non-integer variable declarations, +gotos, etc.) + +

Analysis

+ +

+The analyzer should contain an iterator that analyzes the program +forwards, by induction on the abstract syntax tree. +Loops can be unrolled a fixed number of times (e.g., 3 times), but you +should ultimately use iterations with widening in order to always +terminate for domains with infinite increasing chains. +To increase the precision, the first few (e.g., 3) applications of the +widening may be replaced with a join. + +

+The analysis should be parametric in the choice of a numeric abstract domain. +At least the three following domains must be provided: +

    +
  • the constant domain, that you should implement yourself; +
  • the interval domain, that you should also implement yourself; +
  • the polyhedra domain, which calls the Apron library to perform the abstract operations (you are not asked to implement the polyhedra operators yourself). +
+ +

+Depending on the domain, at least the following kinds of expressions should be handled precisely: +

    +
  • in assignments: all arithmetic expressions for the constant and interval domains; affine expressions for polyhedra; +
  • in the conditions of if-then-else and while instructions: for +polyhedra, boolean formulas whose atoms are affine constraints; for +constants and intervals, boolean formulas whose atoms are simple +comparisons between two variables or between a variable and a constant. +
+ +

+All the expressions allowed in the program syntax must be handled (no +"not implemented" exception); however, any expression not belonging to +the above categories may be handled in a coarse way (e.g., considering +assignments as non-deterministic and ignoring conditions). + +

Output

+ +

+The analysis should at least output a textual file containing: +

    +
  • a list of the assertions that cannot be proved to hold, and their location; +
  • for each print instruction, the invariant found for the specified variables at the location of the instruction. +
+ +

+For debugging, it can be useful to implement a trace mode that outputs the abstract element computed at each step of the analysis. + +

Tests

+ +

+To help you test your analyzer, we provide a set of small test programs, + written in the small language used in the practical sessions. +We also provide the output of their analysis using our reference +analyzer, so that you can easily check the correctness and the precision + of your analyzer. + +

Extensions

+ +

+In addition to the mandatory features described above, you may implement one or several extensions, such as for instance: +

    +
  • functions and function calls (without recursion); +
  • checks for arithmetic overflows and divisions by zero errors in expressions; +
  • other numeric abstract domains (such as non-relational integer congruences, or linear equalities); +
  • several types of numeric variables (such as rationals or floating-point numbers, which are supported directly by Apron); +
  • boolean variables (you can handle them as integer variables that can only take two values: 0 for false, and 1 for true); +
  • arrays (each array can be abstracted by a single variable, and assignments result in weak updates); +
  • non-local control-flow instructions, such as break and continue in loops, forward goto, or even arbitrary goto; +
  • a backward analysis (find necessary conditions on the start of the program so that all assertions are satisfied); +
  • a nicer presentation for the output of the analysis, such as a graphical visualisation of numeric invariants (particularly useful for polyhedra in 2D or 3D); +
  • any extension of your choice. +
+ +

Resources

+ +

Files

+ + +

Documentation

+
    +
  • OCaml programming language; +
  • Menhir parser generator; +
  • ZArith arbitrary precision number library; +
  • Apron abstract domain library; +
  • Mapext maps with some additional useful functions (the source code is included in the codeV1x.tgz bundle). +
+ +

+

+
+

+Author: Antoine Miné +

+ +

+ + + + + \ No newline at end of file diff --git a/doc/enonce_files/main.js b/doc/enonce_files/main.js new file mode 100644 index 0000000..a1e13a0 --- /dev/null +++ b/doc/enonce_files/main.js @@ -0,0 +1,126 @@ +/* + Scripts for my professional web-site: http://www.di.ens.fr/~mine + Copyright (C) Antoine Miné 2011. + */ + + +/* main menu */ +var options = [ + ["img", "antoine_mini.png", "80%", "" ], + ["Antoine Miné", "", "", "" ], + ["br"], + ["Home", "Accueil", "index", "" ], + ["News", "Nouvelles", "index", "#news" ], + ["Research", "Recherche", "index", "#research" ], + ["Habilitation", "Habilitation", "hdr/index", "", "" ], + ["Ph.D", "Thèse", "these/index", "" ], + ["Projects", "Projets", "projects", "" ], + ["Conferences", "Conférences", "confs", "", ], + ["Software", "Logiciels", "index", "#soft", ], + ["Publications", "Publications", "publications", "", "important" ], + ["Talks", "Exposés", "talks", "" ], + ["Teaching", "Enseignement", "index", "#teach", ], + ["Emulation", "Émulation", "emulation", "" ], + ["Contact", "Contact", "index", "#contact" ], + ["-"], +/* + ["SAS 2012", "", "http://www.sas2012.ens.fr", "", "important" ], + ["SSCPS 2012", "", "http://www.sscps.net", ""], + ["SAS 2013", "", "http://research.microsoft.com/en-us/events/sas2013/", ""], +*/ + ["iFM 2014", "", "http://ifm2014.cs.unibo.it/", ""], + ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""], + ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""], + ["TASE 2014", "", "http://www.nudt.edu.cn/tase2014", ""], + ["POPL 2015", "", "http://popl.mpi-sws.org/2015/", ""], + ["-"], + + ["MPRI 2-6 course (M2)", "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""], + ["Semantic course (L3)", "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""], + + ["-"], + ["AstréeA", "", "http://www.astreea.ens.fr", "", "important" ], + ["Astrée", "", "http://www.astree.ens.fr", "" ], + ["Apron", "", "http://apron.cri.ensmp.fr/library", "" ], + ["-"], + ["br"], + ["img", "logo-cnrs.png", "64", "http://www.cnrs.fr" ], + ["br"], + ["img", "logo-ens.png", "82", "http://www.ens.fr" ], + ["br"], + ["img", "logo-inria.png", "128", "http://www.inria.fr" ], +]; + +function print_menu(base,here) +{ + for (var i=0; i\n"); + + else if (options[i][0] == "br") + document.write("
\n"); + + else if (options[i][0] == "img") { + document.write("
"); + if (options[i][3] != "") + document.write(""); + document.write("\"[""); + if (options[i][3] != "") + document.write(""); + document.write("
\n"); + } + + else { + document.write("
"); + var url = options[i][2]; + if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3]; + if (url != "" && url.indexOf(":") == -1) url = base + url; + if (options[i][0] == here || url=="") document.write(""); + else if (4 in options[i]) document.write(""); + else document.write(""); + document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]); + if (options[i][0] == here || url=="") document.write(""); + else document.write(""); + document.write("
\n"); + } + } +} + +function print_ref(s) +{ + document.write(""); + document.write("[" + s + "]"); + document.write(""); +} + +function mailchar(m,i) +{ + var c = ""; + switch (i) { + case 0: c = 'm'; break; + case 1: c = 'i'; break; + case 2: c = 'n'; break; + case 3: c = 'e'; break; + case 4: c = '@'; break; + case 5: c = 'd'; break; + case 6: c = 'i'; break; + case 7: c = '.'; break; + case 8: c = 'e'; break; + case 9: c = 'n'; break; + case 10: c = 's'; break; + case 11: c = '.'; break; + case 12: c = 'f'; break; + case 13: c = 'r'; break; + } + if (c != "") m.innerHTML = m.innerHTML + "" + c + ""; + if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random()); +} + +function main() +{ + var m = document.getElementsByName("mail"); + for (var i=0; i match x with + | AST_stat(stat, _) -> CD.interp_abs(stat) s + | _ -> s) + CD.top_ts + (fst prog) (* parses arguments to get filename *) let main () = -- cgit v1.2.3