Bug 1399763 - add license headers to spec files and make diff work, r=ttaubert

Differential Revision: https://phabricator.services.mozilla.com/D331

5 files changed, 52 insertions, 0 deletions

diff --git a/automation/taskcluster/docker-hacl/Dockerfile b/automation/taskcluster/docker-hacl/Dockerfile
index 46990df3e..8a714398d 100644
--- a/automation/taskcluster/docker-hacl/Dockerfile
+++ b/automation/taskcluster/docker-hacl/Dockerfile
@@ -26,4 +26,5 @@ USER worker
 ENV OPAMYES true
 ENV PATH "/home/worker/hacl-star/dependencies/z3/bin:$PATH"
 ADD setup-user.sh /tmp/setup-user.sh
+ADD license.txt /tmp/license.txt
 RUN bash /tmp/setup-user.sh
diff --git a/automation/taskcluster/docker-hacl/license.txt b/automation/taskcluster/docker-hacl/license.txt
new file mode 100644
index 000000000..03d25c4d3
--- /dev/null
+++ b/automation/taskcluster/docker-hacl/license.txt
@@ -0,0 +1,15 @@
+/* Copyright 2016-2017 INRIA and Microsoft Corporation
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
diff --git a/automation/taskcluster/scripts/run_hacl.sh b/automation/taskcluster/scripts/run_hacl.sh
index 6a186c04e..281075eef 100755
--- a/automation/taskcluster/scripts/run_hacl.sh
+++ b/automation/taskcluster/scripts/run_hacl.sh
@@ -15,6 +15,12 @@ set -e -x -v
 # Verify Poly1305 (doesn't work in docker image build)
 make verify -C ~/hacl-star/code/poly1305 -j$(nproc)
 
+# Add license header to specs
+spec_files=($(find ~/hacl-star/specs -type f -name '*.fst'))
+for f in "${spec_files[@]}"; do
+    cat /tmp/license.txt "$f" > /tmp/tmpfile && mv /tmp/tmpfile "$f"
+done
+
 # Format the extracted C code.
 cd ~/hacl-star/snapshots/nss
 cp ~/nss/.clang-format .
diff --git a/lib/freebl/verified/specs/Spec.CTR.fst b/lib/freebl/verified/specs/Spec.CTR.fst
index fecc53ad5..e411cd353 100644
--- a/lib/freebl/verified/specs/Spec.CTR.fst
+++ b/lib/freebl/verified/specs/Spec.CTR.fst
@@ -1,3 +1,18 @@
+/* Copyright 2016-2017 INRIA and Microsoft Corporation
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
 module Spec.CTR
 
 module ST = FStar.HyperStack.ST
diff --git a/lib/freebl/verified/specs/Spec.Chacha20.fst b/lib/freebl/verified/specs/Spec.Chacha20.fst
index 2cc3ea714..0bdc69725 100644
--- a/lib/freebl/verified/specs/Spec.Chacha20.fst
+++ b/lib/freebl/verified/specs/Spec.Chacha20.fst
@@ -1,3 +1,18 @@
+/* Copyright 2016-2017 INRIA and Microsoft Corporation
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *     http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
 module Spec.Chacha20
 
 module ST = FStar.HyperStack.ST