blob: 07d1a12ec97f83fe43ccab87baa37e2a74483e76 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
open System
open Microsoft.FSharp.Text.Lexing
open System.IO
open ForroPrinter
open Resolver
open Lexer
open Parser
open BoogiePrinter
open Translator
let readAndProcess tracing (filename: string) =
try
if tracing then printfn "Forró: version 1.0" else ()
// lex
let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
let lexbuf = LexBuffer<char>.FromTextReader(f)
lexbuf.EndPos <- { pos_bol = 0;
pos_fname=if filename = null then "stdin" else filename;
pos_cnum=0;
pos_lnum=1 }
// parse
let prog = Parser.start Lexer.tokenize lexbuf
// print the given Forró program
if tracing then
printfn "---------- Given Forró program ----------"
Print prog
else ()
// make sure the program is legal
let rprog = Resolve prog
// translate into Boogie
let bprog = Translate rprog
// print the Boogie program
if tracing then printfn "---------- Resulting Boogie program ----------" else ()
BPrint bprog
// that's it
if tracing then printfn "----------" ; printfn "Done" else ()
with
| ResolutionError(msg) ->
printfn "Resolution error: %s" msg
| ex ->
printfn "Unhandled Exception: %s" ex.Message
let rec start n (args: string []) tracing filename =
if n < args.Length then
let arg = args.[n]
if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()
let filename = if arg.StartsWith "/" then filename else arg
start (n+1) args (tracing || arg = "/trace") filename
else
readAndProcess tracing filename
let args = Environment.GetCommandLineArgs()
start 1 args false null
|
