sic- has quit [Read error: 60 (Operation timed out)]
Excedrin has joined #ocaml
monochrom has quit ["Don't talk to those who talk to themselves."]
Nutssh has quit ["Client exiting"]
Nutssh has joined #ocaml
Nutssh has left #ocaml []
bk_ has quit ["Leaving IRC - dircproxy 1.1.0"]
CosmicRay has joined #ocaml
vezenchio has joined #ocaml
CosmicRay has quit ["Client exiting"]
fab_ has joined #ocaml
ericc has joined #ocaml
_fab has quit [Read error: 110 (Connection timed out)]
cjohnson has quit ["Leaving"]
Xolution has joined #ocaml
mrsolo has joined #ocaml
mrsolo_ has joined #ocaml
grirgz has quit [Read error: 238 (Connection timed out)]
mrsolo has quit [Read error: 113 (No route to host)]
mrsolo_ has quit [Read error: 113 (No route to host)]
mrsolo_ has joined #ocaml
Hipo_ is now known as HIpo
HIpo is now known as Hipo
oracle1 has joined #ocaml
<oracle1>
anyone used cil?
<oracle1>
i wonder how to best compare two parse trees for equality or to compute the difference of two similar parse trees.
smimou has joined #ocaml
kinners has joined #ocaml
jason_ has joined #ocaml
<jason_>
Hm, if I have a function defined in my program that takes a "string->unit." And another piece of code in another module that uses it, if I avoid specifying the type the code will compile 'only' if I use that piece of code in another module. If I don't use it it becomes an unbound type.
<jason_>
If I don't specify types of arguments to my functions will this always be the case?
<jason_>
It would be nice if my module could just be compiled, and that is that.
smimou has quit ["?"]
kinners has quit [Read error: 110 (Connection timed out)]
tea has left #ocaml []
jason_ has quit [Remote closed the connection]
grirgz has joined #ocaml
tomp has quit ["Client Exiting"]
menace has joined #ocaml
budjet has joined #ocaml
budjet has quit [Remote closed the connection]
Iter has joined #ocaml
Hadaka has quit [Read error: 60 (Operation timed out)]
Hipo has quit [Read error: 104 (Connection reset by peer)]
Hipo has joined #ocaml
<oracle1>
anyone used cil?
<oracle1>
i wonder how to best compare two parse trees for equality or to compute the difference of two similar parse trees.
Iter has quit [Read error: 110 (Connection timed out)]
Naked has joined #ocaml
Naked is now known as Hadaka
bk_ has joined #ocaml
pflanze has joined #ocaml
mlh has joined #ocaml
mlh has quit [Client Quit]
<Smerdyakov>
oracle1, you'd probably have to implement it all yourself.
pflanze has quit [Read error: 60 (Operation timed out)]
Submarine has joined #ocaml
<oracle1>
smerdyakov: yes, that's what I expected
<oracle1>
still, somebody might have already The Solution (TM)
<Smerdyakov>
oracle1, well, you can e-mail the authors.
<Smerdyakov>
oracle1, they don't mind. I'm in that research group. :)
<oracle1>
sounds good. So i could address you directly heh
<Smerdyakov>
No, I only use Cil as a user. :)
<oracle1>
that does not count, sorry.
<Smerdyakov>
But my advisor and some of his students are the authors.
<Smerdyakov>
I guess they might not be distributing the source, either.
<oracle1>
ah, you're part of it. at least it sounds interesting
<Submarine>
BLAST? Tom Henzinger's thing?
<Smerdyakov>
I don't know how Astree works, but counterexample-driven predicate abstraction is a pretty cool idea that works quite well. :)
<Smerdyakov>
That is right.
<Submarine>
Smerdyakov, if Patrick Cousot was around, he'd give you examples of where it does not work.
<Smerdyakov>
OK, but it's a nice way of thinking about lots of things.
<Submarine>
Astree is a 'conventional' forward-only abstract interpreter based on denotational semantics.
<Submarine>
it has naive notions of memory and pointers
<Submarine>
a very fast interval analysis
<Submarine>
and a bunch of specialized domains
<Submarine>
and a ton of extra tricks
<Smerdyakov>
BLAST uses a very general framework within the model checker and relies on a theorem prover to do the specialized stuff.
<Submarine>
I know. You use SIMPLIFY. :-)
<Smerdyakov>
There are other theorem provers that you can use, as well.
<Submarine>
I actually saw Henzinger one week ago explaining how you looked for the cut in the contradiction.
<Smerdyakov>
Yeah. That depends on using the Foci theorem prover.
<Smerdyakov>
Which applies that model theoretic result whose name I forget now.
<Smerdyakov>
Ah. "Craig's interpolation theorem."
<Submarine>
exactly
<Submarine>
still, it's some of a mystery to me how you choose the predicate to use
<Smerdyakov>
It's easy, I think.
<Smerdyakov>
You ask the theorem prover to prove that the supposed error trace you've found in invalid.
<Smerdyakov>
If it proves it, you add every predicate found in the proof.
<Submarine>
and the "focus" thing just restricts to the predicates used for the proof that the "cut" is false
<Smerdyakov>
It restricts the part of the proof that are relevant to each program point found in the trace, yes.
* Smerdyakov
leaves for a bit.
<oracle1>
i would like to have a generic function which returns the argument of a constructor
<Submarine>
eeew?
<oracle1>
but that's probably not possible like i want it..
<Smerdyakov>
oracle1, it's hard to tell why you want that, but the usual way to avoid inconveniences associated with such things is to write a fold function over your custom data type.
<Submarine>
I don't understand what oracle1 wants.
<oracle1>
e.g. when I give the function this as argument: CallA(CallB(CallA(A(10))))
<oracle1>
it should return CallB(CallA(A(10))).
<Submarine>
oooh
<Submarine>
it's plain old pattern matching
<oracle1>
this works fine as long as the argument of the constructor is of the same type
bk_ has quit [Remote closed the connection]
bk_ has joined #ocaml
<Submarine>
?!?
<oracle1>
well given these two types
<oracle1>
type a = A of int | CallB of b | Empty
<oracle1>
and b = B of int | CallA of a
<oracle1>
how would you write a function next_b which returns the next argument of a b type ?
<oracle1>
but maybe I have the wrong problems heh..or I have to do it differently in ocaml
<Submarine>
oracle1, you have the wrong problems
<Submarine>
or you *might* use polymorphic variants