diff --git a/Makefile.in b/Makefile.in index 58842022bf7c94d373d4a3818c5a1c539150dc64..a45d783fa36145043b64faae7b4f15b6fb84b5a4 100644 --- a/Makefile.in +++ b/Makefile.in @@ -1986,7 +1986,8 @@ headers: headers-coq src/*/*.ml src/*/*.ml[iyl4] \ plugins/*/*.ml plugins/*/*.ml[ily] \ lib/coq-tactic/*.v lib/coq/*.v \ - src/tools/cpulimit.c \ + src/server/*.c src/server/*.h \ + src/ide/resetgc.c \ examples/use_api/*.ml headers-coq: diff --git a/src/driver/prove_client.ml b/src/driver/prove_client.ml index 63cab2adfafc2d68e3ac6b6f1ab82cc158d82ddb..b4e2b87dd2d180f1767daadee0ed0d0890859510 100644 --- a/src/driver/prove_client.ml +++ b/src/driver/prove_client.ml @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + let socket : Unix.file_descr option ref = ref None exception NotConnected diff --git a/src/driver/prove_client.mli b/src/driver/prove_client.mli index c9c4d167d5892f369d14270a1a8ac494ba058ded..ecb701fb9adbf8312c48e41868e673a875255821 100644 --- a/src/driver/prove_client.mli +++ b/src/driver/prove_client.mli @@ -1,3 +1,14 @@ +(********************************************************************) +(* *) +(* The Why3 Verification Platform / The Why3 Development Team *) +(* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University *) +(* *) +(* This software is distributed under the terms of the GNU Lesser *) +(* General Public License version 2.1, with the special exception *) +(* on linking described in file LICENSE. *) +(* *) +(********************************************************************) + exception NotConnected exception AlreadyConnected exception InvalidAnswer of string diff --git a/src/ide/resetgc.c b/src/ide/resetgc.c index 070a3a5137b595aeafff637b08a81a5016769d6f..766001a79044bdddfda3f9b6f97bf35cec2607b6 100644 --- a/src/ide/resetgc.c +++ b/src/ide/resetgc.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include diff --git a/src/server/arraylist.c b/src/server/arraylist.c index 5ef40769dbaa4caf0c7224826843f2d82c170b51..6c88091c87959c910bea411d3ea35e46be21bed4 100644 --- a/src/server/arraylist.c +++ b/src/server/arraylist.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include "arraylist.h" diff --git a/src/server/arraylist.h b/src/server/arraylist.h index c9f33cafb68ed0d3370a2c882b76e740cb72eb07..bc68b44951a24b51a97f3f22e3cffa2b10a677c9 100644 --- a/src/server/arraylist.h +++ b/src/server/arraylist.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef ARRAYLIST_H #define ARRAYLIST_H diff --git a/src/server/logging.c b/src/server/logging.c index 31586c9247df42f0ce5a5c5fdb39303fb08d65ee..68578a9a4282a0aae1e845e2be7f236df8c9926d 100644 --- a/src/server/logging.c +++ b/src/server/logging.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include "logging.h" diff --git a/src/server/logging.h b/src/server/logging.h index 7ec3965204f2b9ad9a7a2a2c7f089f3cde36647f..16e94f5fbcdafd1e73d832eae555d24a6f7b1dbf 100644 --- a/src/server/logging.h +++ b/src/server/logging.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef LOGGING_H #define LOGGING_H diff --git a/src/server/options.c b/src/server/options.c index 6b6ce3bef94afa0855bc1d9e9203f230d72def8d..47a8d967a80b9d53b811fe62fd0af80a819647bb 100644 --- a/src/server/options.c +++ b/src/server/options.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include diff --git a/src/server/options.h b/src/server/options.h index 167c94887b6f06dfc8d30a11a1aa0c037925b4df..8799f00abc6d838bfcc1bd20ad53244872c15f26 100644 --- a/src/server/options.h +++ b/src/server/options.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef OPTIONS_H #define OPTIONS_H diff --git a/src/server/queue.c b/src/server/queue.c index f5e57fda1c0f172a0dd3fd1e17b7ba59f0226709..9aad10192d32326d5420a04b373e07776cc4eeee 100644 --- a/src/server/queue.c +++ b/src/server/queue.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include "queue.h" diff --git a/src/server/queue.h b/src/server/queue.h index fd33749c40a4c576fcab27894443898c967d04a6..f87b44f133c2677488b4dc9e93bcc934105799e7 100644 --- a/src/server/queue.h +++ b/src/server/queue.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef QUEUE_H #define QUEUE_H diff --git a/src/server/readbuf.c b/src/server/readbuf.c index faadd05a7ec5af8aa2782657bf1033f480ea5aae..91d1bc6f95bd43d4ca14e536a6ddf7c195ba656f 100644 --- a/src/server/readbuf.c +++ b/src/server/readbuf.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include diff --git a/src/server/readbuf.h b/src/server/readbuf.h index 7a24d066485c06d1d1c9b9b61a9ed9127540e7a1..e43d35fe792b53890ecf6e2c7d352e945faabf0b 100644 --- a/src/server/readbuf.h +++ b/src/server/readbuf.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef READBUF_H #define READBUF_H diff --git a/src/server/request.c b/src/server/request.c index 8ef2fe700c99b9b36a51bdf11a72588196527f44..3674e8e6dd546a8f776a0e27093ff70a2e47a0b3 100644 --- a/src/server/request.c +++ b/src/server/request.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include diff --git a/src/server/request.h b/src/server/request.h index 0e174e0af93396ecdcf3479e7a9c34dbdf6aaf15..fd413725799d15e884efbd29d4694cc2aaf1ad46 100644 --- a/src/server/request.h +++ b/src/server/request.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef REQUEST_H #define REQUEST_H diff --git a/src/server/server-unix.c b/src/server/server-unix.c index b60df36494682f2ed38c54f9317d0a8dad424bbe..87ae5e183b44aa03fbace66e49a9dd259cbbd040 100644 --- a/src/server/server-unix.c +++ b/src/server/server-unix.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + // This is the unix implementation of the VC server. It uses the poll // mechanism to wait for events, plus the "self pipe trick" to handle // terminating child processes. diff --git a/src/server/server-win.c b/src/server/server-win.c index 6319ad2798f23c657f04e31c057b4ae829ead771..93e06d5106b95a71a512aeccd6554b3a306a1132 100644 --- a/src/server/server-win.c +++ b/src/server/server-win.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + // This is the windows implementation of the VC server. Its main feature is // the use of an IO Completion port to handle all kinds of events. // diff --git a/src/server/writebuf.c b/src/server/writebuf.c index da75830bd6e30104d76fa4fe9418e91f0341901a..5739952b18368ee4566e3690e62f6eb9ceb345cf 100644 --- a/src/server/writebuf.c +++ b/src/server/writebuf.c @@ -1,3 +1,14 @@ +/********************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/********************************************************************/ + #include #include #include diff --git a/src/server/writebuf.h b/src/server/writebuf.h index e2ad2eb49c288c37d50407abefd4c52be0a13b39..3a73096cb6d3700b0eb7efaa2fd19336880d34dc 100644 --- a/src/server/writebuf.h +++ b/src/server/writebuf.h @@ -1,3 +1,14 @@ +/**************************************************************************/ +/* */ +/* The Why3 Verification Platform / The Why3 Development Team */ +/* Copyright 2010-2016 -- INRIA - CNRS - Paris-Sud University */ +/* */ +/* This software is distributed under the terms of the GNU Lesser */ +/* General Public License version 2.1, with the special exception */ +/* on linking described in file LICENSE. */ +/* */ +/**************************************************************************/ + #ifndef WRITEBUF_H #define WRITEBUF_H