From ee196e3ca4e1190a9e869b795d2b6a669e623330 Mon Sep 17 00:00:00 2001 From: Alexandre Oliva Date: Sat, 1 Feb 2014 04:31:05 -0200 Subject: [PATCH] * manual/check-safety.sh: New. * manual/Makefile ($(objpfx)stamp-summary): Run it. --- ChangeLog | 5 +++ manual/Makefile | 3 +- manual/check-safety.sh | 119 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 126 insertions(+), 1 deletion(-) create mode 100644 manual/check-safety.sh diff --git a/ChangeLog b/ChangeLog index d22af7a..4516c2a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2014-02-01 Alexandre Oliva + * manual/check-safety.sh: New. + * manual/Makefile ($(objpfx)stamp-summary): Run it. + +2014-02-01 Alexandre Oliva + * manual/terminal.texi: Document MTASC-safety properties. 2014-02-01 Alexandre Oliva diff --git a/manual/Makefile b/manual/Makefile index 3037303..5f98b2a 100644 --- a/manual/Makefile +++ b/manual/Makefile @@ -88,6 +88,7 @@ $(objpfx)libc/index.html: $(addprefix $(objpfx),$(libc-texi-generated)) $(objpfx)summary.texi: $(objpfx)stamp-summary ; $(objpfx)stamp-summary: summary.awk $(filter-out $(objpfx)summary.texi, \ $(texis-path)) + -$(SHELL) ./check-safety.sh $(filter-out $(objpfx)%, $(texis-path)) $(AWK) -f $^ | sort -t' ' -df -k 1,1 | tr '\014' '\012' \ > $(objpfx)summary-tmp $(move-if-change) $(objpfx)summary-tmp $(objpfx)summary.texi @@ -157,7 +158,7 @@ $(objpfx)%.pdf: %.texinfo # Distribution. minimal-dist = summary.awk texis.awk tsort.awk libc-texinfo.sh libc.texinfo \ - libm-err.texi stamp-libm-err \ + libm-err.texi stamp-libm-err check-safety.sh \ $(filter-out summary.texi, $(nonexamples)) \ $(patsubst %.c.texi,examples/%.c, $(examples)) diff --git a/manual/check-safety.sh b/manual/check-safety.sh new file mode 100644 index 0000000..701624d --- /dev/null +++ b/manual/check-safety.sh @@ -0,0 +1,119 @@ +#! /bin/sh + +# Copyright 2014 Free Software Foundation, Inc. +# This file is part of the GNU C Library. + +# The GNU C Library is free software; you can redistribute it and/or +# modify it under the terms of the GNU Lesser General Public +# License as published by the Free Software Foundation; either +# version 2.1 of the License, or (at your option) any later version. + +# The GNU C Library is distributed in the hope that it will be useful, +# but WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +# Lesser General Public License for more details. + +# You should have received a copy of the GNU Lesser General Public +# License along with the GNU C Library; if not, see +# . + + +# Check that the @safety notes are self-consistent, i.e., that they're +# in proper order (mt then as then ac), that remarks appear within +# corresponding sections (mt within mt, etc), that unsafety always has +# an explicit reason and when there's a reason for unsafety it's not +# safe, and that there aren't duplicates remarks. + + +success=: + +# If no arguments are given, take all *.texi files in the current directory. +test $# != 0 || set *.texi + +# Check that all safety remarks have entries for all of MT, AS and AC, +# in this order, with an optional prelim note before them. +grep -n '^@safety' "$@" | +grep -v ':@safety{\(@prelim{}\)\?@mt\(un\)\?safe{.*}'\ +'@as\(un\)\?safe{.*}@ac\(un\)\?safe{.*}}' && +success=false + +# Check that @mt-started notes appear within @mtsafe or @mtunsafe, +# that @as-started notes appear within @assafe or @asunsafe, and that +# @ac-started notes appear within @acsafe or @acunsafe. Also check +# that @mt, @as and @ac are followed by an s (for safe) or u (for +# unsafe), but let @mt have as, ac or asc before [su], and let @as +# have a c (for cancel) before [su]. Also make sure blanks separate +# each of the annotations. +grep -n '^@safety' "$@" | +grep -v ':@safety{\(@prelim{}\)\?'\ +'@mt\(un\)\?safe{\(@mt\(asc\?\|ac\)\?[su][^ ]*}\)\?'\ +'\( @mt\(asc\?\|ac\)\?[su][^ ]*}\)*}'\ +'@as\(un\)\?safe{\(@asc\?[su][^ ]*}\)\?'\ +'\( @asc\?[su][^ ]*}\)*}'\ +'@ac\(un\)\?safe{\(@ac[su][^ ]*}\)\?'\ +'\( @ac[su][^ ]*}\)*}}' && +success=false + +# Make sure safety lines marked as @mtsafe do not contain any +# MT-Unsafe remark; that would be @mtu, but there could be as, ac or +# asc between mt and u. +grep -n '^@safety.*@mtsafe' "$@" | +grep '@mt\(asc\?\|ac\)?u' "$@" && +success=false + +# Make sure @mtunsafe lines contain at least one @mtu remark (with +# optional as, ac or asc between mt and u). +grep -n '^@safety.*@mtunsafe' "$@" | +grep -v '@mtunsafe{.*@mt\(asc\?\|ac\)\?u' && +success=false + +# Make sure safety lines marked as @assafe do not contain any AS-Unsafe +# remark, which could be @asu or @mtasu note (with an optional c +# between as and u in both cases). +grep -n '^@safety.*@assafe' "$@" | +grep '@\(mt\)\?asc\?u' && +success=false + +# Make sure @asunsafe lines contain at least one @asu remark (which +# could be @ascu, or @mtasu or even @mtascu). +grep -n '^@safety.*@asunsafe' "$@" | +grep -v '@mtasc\?u.*@asunsafe\|@asunsafe{.*@asc\?u' && +success=false + +# Make sure safety lines marked as @acsafe do not contain any +# AC-Unsafe remark, which could be @acu, @ascu or even @mtacu or +# @mtascu. +grep -n '^@safety.*@acsafe' "$@" | +grep '@\(mt\)\?as\?cu' && +success=false + +# Make sure @acunsafe lines contain at least one @acu remark (possibly +# implied by @ascu, @mtacu or @mtascu). +grep -n '^@safety.*@acunsafe' "$@" | +grep -v '@\(mtas\?\|as\)cu.*@acunsafe\|@acunsafe{.*@acu' && +success=false + +# Make sure there aren't duplicate remarks in the same safety note. +grep -n '^@safety' "$@" | +grep '[^:]\(@\(mt\|a[sc]\)[^ {]*{[^ ]*}\).*[^:]\1' && +success=false + +# Check that comments containing safety remarks do not contain {}s, +# that all @mt remarks appear before @as remarks, that in turn appear +# before @ac remarks, all properly blank-separated, and that an +# optional comment about exclusions is between []s at the end of the +# line. +grep -n '^@c \+[^@ ]\+\( dup\)\?'\ +'\( @\(mt\|a[sc]\)[^ ]*\)*\( \[.*\]\)\?$' "$@" | +grep -v ':@c *[^@{}]*\( @mt[^ {}]*\)*'\ +'\( @as[^ {}]*\)*\( @ac[^ {}]*\)*\( \[.*\]\)\?$' && +success=false + +# Check that comments containing safety remarks do not contain +# duplicate remarks. +grep -n '^@c \+[^@ ]\+\( dup\)\?'\ +'\( @\(mt\|a[sc]\)[^ ]*\)*\( \[.*\]\)\?$' "$@" | +grep '[^:]\(@\(mt\|a[sc]\)[^ ]*\) \(.*[^:]\)\?\1\($\| \)' && +success=false + +$success -- 2.7.4